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/

[1] I. S. Anureev, I. V. Maryasov, V. A. Nepomniaschy, “C-programs Verification Based on Mixed Axiomatic Semantics”, Automatic Control and Computer Sciences, 45:7 (2011), 485–500 | DOI

[2] C. Barrett, C. L., Conway, M. Deters, L. Hadarean, D. Jovanović, T. King, A. Reynolds, C. Tinelli, “CVC4”, 23rd Int. Conf. CAV, Lecture Notes in Computer Science, 6806, 2011, 171–177 | DOI | MR

[3] E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, S. Tobies, “VCC: A Practical System for Verifying Concurrent C”, 22nd Int. Conf. TPHOLs, Lecture Notes in Computer Science, 5674, 2009, 23–42 | DOI | MR

[4] J.-C. Filliâtre, C. Marché, “Multi-prover Verification of C Programs”, 6th ICFEM, Lecture Notes in Computer Science, 3308, 2004, 15–29 | DOI

[5] D. A. Kondratyev, “The Extension of the MetaVCG Approach by Semantic Mark-up Concept”, Int. Workshop-conf. “Tools Methods of Program Analysis” (St. Petersburg, 2015), 107–118

[6] K. R. M. Leino, “Automating Induction with an SMT Solver”, 13th Int. Conf. VMCAI, Lecture Notes in Computer Science, 7148, 2012, 315–331 | DOI | MR | Zbl

[7] I. V. Maryasov, V. A. Nepomniaschy, “Loop Invariants Elimination for Definite Iterations over Unchangeable Data Structures in C Programs”, Modeling and Analysis of Information Systems, 22:6 (2015), 773–782 | DOI | MR

[8] I. V. Maryasov, V. A. Nepomniaschy, D. A. Kondratyev, “Verification of Definite Iteration over Arrays with a Loop Exit in C Programs”, System Informatics, 2017, no. 10, 57–66

[9] I. V. Maryasov, V. A. Nepomniaschy, A. V. Promsky, D. A. Kondratyev, “Automatic C Program Verification Based on Mixed Axiomatic Semantics”, Automatic Control and Computer Sciences, 48:7 (2014), 407–414 | DOI

[10] M. Moriconi, R. L. Schwarts, “Automatic Construction of Verification Condition Generators From Hoare Logics”, Automata, Languages and Programming, Lecture Notes in Computer Science, 115, 1981, 363–377 | DOI | MR | Zbl

[11] V. A. Nepomniaschy, “Verification of Definite Iteration over Hierarchical Data Structures”, FASE/ETAPS, Lecture Notes in Computer Science, 1577, 1999, 176–187 | DOI | MR

[12] A. Reynolds, V. Kuncak, “Induction for SMT solvers”, 16th Int. Conf. VMCAI, Lecture Notes in Computer Science, 8931, 2015, 80–98 | DOI | MR | Zbl

[13] T. Tuerk, “Local Reasoning about While-Loops”, VSTTE 2010, 29–39