Towards the ’verified verifier’. Theory and practice
D. A. Kondratyeva, A. V. Promskyb
a Novosibirsk State University, ul. Pirogova, 2, Novosibirsk, 630090, Russia
b A. P. Ershov Institute of Informatics Systems SB RAS,
Acad. Lavrentjev pr., 6, Novosibirsk, 630090, Russia
As opposed to traditional testing, the deductive verification represents a formal way to examine the program correctness. But what about the correctness of the verification system itself? The theoretical foundations of Hoare's logic were examined in classical works, and some soundness/completeness theorems are well-known. However, we practically are not aware of implementations of those theoretical methods which were subjected to anything more than testing. In other words, our ultimate goal is a verification system which can be self-applicable (at least partially). In our recent studies we addressed ourselves to the metageneration approach in order to make such a task more feasible.
verification, specification, axiomatic semantics, the C-light language, verification condition, MetaVCG.
PDF file (504 kB)
D. A. Kondratyev, A. V. Promsky, “Towards the ’verified verifier’. Theory and practice”, Model. Anal. Inform. Sist., 21:6 (2014), 71–82
Citation in format AMSBIB
\by D.~A.~Kondratyev, A.~V.~Promsky
\paper Towards the ’verified verifier’. Theory and practice
\jour Model. Anal. Inform. Sist.
Citing articles on Google Scholar:
Related articles on Google Scholar:
|Number of views:|