Geodesic
Towards the ’verified verifier’. Theory and practice
Modelirovanie i analiz informacionnyh sistem, Tome 21 (2014) no. 6, pp. 71-82.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: verification, specification, axiomatic semantics, the C-light language, verification condition, MetaVCG. 
@article{MAIS_2014_21_6_a6,
     author = {D. A. Kondratyev and A. V. Promsky},
     title = {Towards the {\textquoteright}verified verifier{\textquoteright}. {Theory} and practice},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {71--82},
     publisher = {mathdoc},
     volume = {21},
     number = {6},
     year = {2014},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2014_21_6_a6/}
}
TY  - JOUR
AU  - D. A. Kondratyev
AU  - A. V. Promsky
TI  - Towards the ’verified verifier’. Theory and practice
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2014
SP  - 71
EP  - 82
VL  - 21
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2014_21_6_a6/
LA  - ru
ID  - MAIS_2014_21_6_a6
ER  - 
%0 Journal Article
%A D. A. Kondratyev
%A A. V. Promsky
%T Towards the ’verified verifier’. Theory and practice
%J Modelirovanie i analiz informacionnyh sistem
%D 2014
%P 71-82
%V 21
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2014_21_6_a6/
%G ru
%F MAIS_2014_21_6_a6
D. A. Kondratyev; A. V. Promsky. Towards the ’verified verifier’. Theory and practice. Modelirovanie i analiz informacionnyh sistem, Tome 21 (2014) no. 6, pp. 71-82. http://geodesic.mathdoc.fr/item/MAIS_2014_21_6_a6/

[1] K. R. Apt, E. R. Olderog, Verification of sequential and concurrent programs, Springer, Berlin etc., 1991, 450 pp. | MR | Zbl

[2] E. Cohen, M. Dahlweid, M. A. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, S. Tobies, “VCC: A Practical System for Verifying Concurrent C”, Proc. TPHOLs (2009), LNCS, 5674, 2009, 23–42 | MR

[3] J. C. Filliâtre, C. Marché, “Multi-prover verification of C programs”, Proc. ICFEM (2004), LNCS, 3308, 2004, 15–29

[4] I. V. Maryasov, V. A. Nepomnyaschy, A. V. Promsky, D. A. Kondratyev, “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), 50–59

[5] M. Moriconi, R. L. Schwartz, “Automatic Construction of Verification Condition Generators From Hoare Logics”, Lect. Notes Comput. Sci., 115, Berlin etc., 1981, 363–377 | DOI | MR | Zbl

[6] Nepomnyaschy V. A., Anureev I. S., Mikhaylov I. N., Promsky A. V., “Orientirovannyy na verifikatsiyu yazyk C-light”, Formal'nye metody i modeli informatiki, Sb. nauch. tr., Sistemnaya informatika, 9, Izdatel'stvo SO RAN, Novosibirsk, 2004, 51–134 (in Russion)

[7] M. Norrish, C formalised in HOL, Thes. doct. phylosophy (computer sci.), Cambridge, 1998, 150 pp.

[8] D. von Oheimb, “Hoare logic for Java in Isabelle/HOL”, Concurrency and Computation: Practice and Experience, 13:13 (2001)

[9] A. V. Promsky, “C Program Verification: Verification Condition Explanation and Standard Library”, Automatic Control and Computer Sciences, 46:7 (2012), 394–401 | DOI

[10] A. V. Promsky, “Experiments on self-applicability in the C-light verification system”, Bull. Nov. Comp. Center, Comp. Science, 35 (2013), 85–99