Towards the ’Verified Verifier’. Theory and Practice
https://doi.org/10.18255/1818-1015-2014-6-71-82
Abstract
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.
About the Authors
D. A. Kondratyev
Novosibirsk State University
Russian Federation
студент, ul. Pirogova, 2, Novosibirsk, 630090, Russia
Russian Federation
студент, ul. Pirogova, 2, Novosibirsk, 630090, Russia
A. V. Promsky
A.P. Ershov Institute of Informatics Systems SB RAS
Russian Federation
ст. науч. сотр., Acad. Lavrentjev pr., 6, Novosibirsk, 630090, Russia
Russian Federation
ст. науч. сотр., Acad. Lavrentjev pr., 6, Novosibirsk, 630090, Russia
References
1. Apt K.R., Olderog E.R. Verification of sequential and concurrent programs. Berlin etc.: Springer, 1991. 450 p.
2. Cohen E., Dahlweid M., Hillebrand M.A., Leinenbach D., Moskal M., Santen T., Schulte W., Tobies S. VCC: A Practical System for Verifying Concurrent C // Proc. TPHOLs. 2009. LNCS. 2009. Vol. 5674. P. 23–42.
3. Filliˆatre J.C., March´e C. Multi-prover verification of C programs // Proc. ICFEM 2004. LNCS. 2004. Vol. 3308. P. 15–29.
4. Maryasov I.V., Nepomnyaschy V.A., Promsky A.V., Kondratyev D.A. Automatic C Program Verification Based on Mixed Axiomatic Semantics // Proc. Fourth Workshop "Program Semantics, Specification and Verification: Theory and Applications". Yekaterinburg, Russia, June 24, 2013. P. 50–59.
5. Moriconi M., Schwartz R.L. Automatic Construction of Verification Condition Generators From Hoare Logics // Lect. Notes Comput. Sci. Berlin etc., 1981. Vol. 115. P. 363–377.
6. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Системная информатика: Сб. науч. тр. Новосибирск: Издательство СО РАН, 2004. Вып. 9: Формальные методы и модели информатики. С. 51–134. [Nepomnyaschy V.A., Anureev I.S., Mikhaylov I.N., Promsky A.V. Orientirovannyy na verifikatsiyu yazyk C-light // Sistemnaya informatika: Sb. nauch. tr. Novosibirsk: Izdatel’stvo SO RAN, 2004. Vyp. 9: Formal’nye metody i modeli informatiki. S. 51–134 (in Russion)].
7. Norrish M. C formalised in HOL: Thes. doct. phylosophy (computer sci.). Cambridge, 1998. 150 p.
8. Oheimb D. von. Hoare logic for Java in Isabelle/HOL // Concurrency and Computation: Practice and Experience. 2001. 13(13).
9. Promsky A.V. C Program Verification: Verification Condition Explanation and Standard Library // Automatic Control and Computer Sciences. 2012. Vol. 46, No. 7. P. 394–401.
10. Promsky A.V. Experiments on self-applicability in the C-light verification system // Bull. Nov. Comp. Center, Comp. Science. 2013. 35. P. 85–99.
Review
For citations:
Kondratyev D.A., Promsky A.V. Towards the ’Verified Verifier’. Theory and Practice. Modeling and Analysis of Information Systems. 2014;21(6):71-82. (In Russ.) https://doi.org/10.18255/1818-1015-2014-6-71-82
Views:
970
Email this article 