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/