Geodesic
Loop invariants elimination for definite iterations over unchangeable data structures in C programs
Modelirovanie i analiz informacionnyh sistem, Tome 22 (2015) no. 6, pp. 773-782

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

The C-program verification is an urgent problem of modern programming. To apply known methods of deductive verification it is necessary to provide loop invariants which might be a challenge in many cases. In this paper we consider the C-light language [18] which is a powerful subset of the ISO C language. To verify C-light programs the two-level approach [19, 20] and the mixed axiomatic semantics method [1, 3, 11] were suggested. At the first stage, we translate [17] the source C-light program into C-kernel one. The C-kernel language [19] is a subset of C-light. The theorem of translation correctness was proved in [10, 11]. The C-kernel has less statements with respect to the C-light, this allows to decrease the number of inference rules of axiomatic semantics during its development. At the second stage of this approach, the verification conditions are generated by applying the rules of mixed axiomatic semantics [10, 11] which could contain several rules for the same program statement. In such cases the inference rules are applied depending on the context. Let us note that application of the mixed axiomatic semantics allows to significantly simplify verification conditions in many cases. This article represents an extension of this approach which includes our verification method for definite iteration over unchangeable data structures without loop exit in C-light programs. The method contains a new inference rule for the deifinite iteration without invariants. This rule was implemented in verification conditions generator. At the proof stage the SMT-solver Z3 [12] is used. An example which illustrates the application of this technique is considered. The article is published in the authors' wording.
Keywords: C-light, mixed axiomatic semantics, definite iteration, specification, verification, Hoare logic.
Mots-clés : loop invariants, unchangeable data structures, Z3 
@article{MAIS_2015_22_6_a3,
     author = {I. V. Maryasov and V. A. Nepomniaschy},
     title = {Loop invariants elimination for definite iterations over unchangeable data structures in {C} programs},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {773--782},
     publisher = {mathdoc},
     volume = {22},
     number = {6},
     year = {2015},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2015_22_6_a3/}
}
TY  - JOUR
AU  - I. V. Maryasov
AU  - V. A. Nepomniaschy
TI  - Loop invariants elimination for definite iterations over unchangeable data structures in C programs
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2015
SP  - 773
EP  - 782
VL  - 22
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2015_22_6_a3/
LA  - en
ID  - MAIS_2015_22_6_a3
ER  - 
%0 Journal Article
%A I. V. Maryasov
%A V. A. Nepomniaschy
%T Loop invariants elimination for definite iterations over unchangeable data structures in C programs
%J Modelirovanie i analiz informacionnyh sistem
%D 2015
%P 773-782
%V 22
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2015_22_6_a3/
%G en
%F MAIS_2015_22_6_a3
I. V. Maryasov; V. A. Nepomniaschy. Loop invariants elimination for definite iterations over unchangeable data structures in C programs. Modelirovanie i analiz informacionnyh sistem, Tome 22 (2015) no. 6, pp. 773-782. http://geodesic.mathdoc.fr/item/MAIS_2015_22_6_a3/