Geodesic
Invariant elimination of definite iterations over arrays in C programs verification
Modelirovanie i analiz informacionnyh sistem, Tome 24 (2017) no. 6, pp. 743-754

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

This work represents the further development of the method for definite iteration verification [7]. It extends the mixed axiomatic semantics method [1] suggested for C-light program verification. This extension includes a verification method for definite iteration over unchangeable arrays with a loop exit in C-light programs. The method includes an inference rule for the iteration without invariants, which uses a special function that expresses loop body. This rule was implemented in verification conditions generator, which is the part of our C-light verification system. To prove generated verification conditions an induction is applied which is a challenge for SMT-solvers. At proof stage the SMT-solver CVC4 is used in our verification system. To overcome mentioned difficulty a rewriting strategy for verification conditions is suggested. A method based on theory extension by new theorems to prove verification conditions is suggested. An example, which illustrates the application of these methods, is considered. The article is published in the authors’ wording.
Keywords: C-light, mixed axiomatic semantics, definite iteration, arrays, CVC4, specification, verification, Hoare logic.
Mots-clés : loop invariants 
@article{MAIS_2017_24_6_a6,
     author = {I. V. Maryasov and V. A. Nepomniaschy and D. A. Kondratyev},
     title = {Invariant elimination of definite iterations over arrays in {C} programs verification},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {743--754},
     publisher = {mathdoc},
     volume = {24},
     number = {6},
     year = {2017},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2017_24_6_a6/}
}
TY  - JOUR
AU  - I. V. Maryasov
AU  - V. A. Nepomniaschy
AU  - D. A. Kondratyev
TI  - Invariant elimination of definite iterations over arrays in C programs verification
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2017
SP  - 743
EP  - 754
VL  - 24
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2017_24_6_a6/
LA  - en
ID  - MAIS_2017_24_6_a6
ER  - 
%0 Journal Article
%A I. V. Maryasov
%A V. A. Nepomniaschy
%A D. A. Kondratyev
%T Invariant elimination of definite iterations over arrays in C programs verification
%J Modelirovanie i analiz informacionnyh sistem
%D 2017
%P 743-754
%V 24
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2017_24_6_a6/
%G en
%F MAIS_2017_24_6_a6
I. V. Maryasov; V. A. Nepomniaschy; D. A. Kondratyev. Invariant elimination of definite iterations over arrays in C programs verification. Modelirovanie i analiz informacionnyh sistem, Tome 24 (2017) no. 6, pp. 743-754. http://geodesic.mathdoc.fr/item/MAIS_2017_24_6_a6/