Geodesic
The complex approach of the C-lightVer system to the automated error localization in C-programs
Modelirovanie i analiz informacionnyh sistem, Tome 26 (2019) no. 4, pp. 502-519

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

The C-lightVer system for the deductive verification of C programs is being developed at the IIS SB RAS. Based on the two-level architecture of the system, the C-light input language is translated into the intermediate C-kernel language. The meta generator of the correctness conditions receives the C-kernel program and Hoare logic for the C-kernel as input. To solve the well-known problem of determining loop invariants, the definite iteration approach was chosen. The body of the definite iteration loop is executed once for each element of the finite dimensional data structure, and the inference rule for them uses the substitution operation rep, which represents the action of the cycle in symbolic form. Also, in our meta generator, the method of semantic markup of correctness conditions has been implemented and expanded. It allows to generate explanations for unproven conditions and simplifies the errors localization. Finally, if the theorem prover fails to determine the truth of the condition, we can focus on proving its falsity. Thus a method of proving the falsity of the correctness conditions in the ACL2 system was developed. The need for more detailed explanations of the correctness conditions containing the replacement operation rep has led to a change of the algorithms for generating the replacement operation, and the generation of explanations for unproven correctness conditions. Modifications of these algorithms are presented in the article. They allow marking rep definition with semantic labels, extracting semantic labels from rep definition and generating description of break execution condition.
Keywords: deductive verification, semantic label, error localization, C-lightVer, MetaVCG, definite iteration, proof strategy.
Mots-clés : ACL2 
@article{MAIS_2019_26_4_a3,
     author = {D. A. Kondratyev and A. V. Promsky},
     title = {The complex approach of the {C-lightVer} system to the automated error localization in {C-programs}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {502--519},
     publisher = {mathdoc},
     volume = {26},
     number = {4},
     year = {2019},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a3/}
}
TY  - JOUR
AU  - D. A. Kondratyev
AU  - A. V. Promsky
TI  - The complex approach of the C-lightVer system to the automated error localization in C-programs
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2019
SP  - 502
EP  - 519
VL  - 26
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a3/
LA  - ru
ID  - MAIS_2019_26_4_a3
ER  - 
%0 Journal Article
%A D. A. Kondratyev
%A A. V. Promsky
%T The complex approach of the C-lightVer system to the automated error localization in C-programs
%J Modelirovanie i analiz informacionnyh sistem
%D 2019
%P 502-519
%V 26
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a3/
%G ru
%F MAIS_2019_26_4_a3
D. A. Kondratyev; A. V. Promsky. The complex approach of the C-lightVer system to the automated error localization in C-programs. Modelirovanie i analiz informacionnyh sistem, Tome 26 (2019) no. 4, pp. 502-519. http://geodesic.mathdoc.fr/item/MAIS_2019_26_4_a3/