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/

[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] I. Anureev, I. Maryasov, V. Nepomniaschy, “Revised Mixed Axiomatic Semantics Method of C Program Verification”, Third Workshop “Program Semantics, Specification and Verification: Theory and Applications”, PSSV 2012, Proceedings (Nizhni Novgorod, Russia, July 1–2), eds. V. Nepomniaschy, V. Sokolov, 2012, 16–23

[3] I. S. Anureev, I. V. Maryasov, V. A. Nepomniaschy, “Two-level Mixed Verification Method of C-light Programs in Terms of Safety Logic”, Bulletin of the Novosibirsk Computing Center. Ser. Computer Science, 34 (2012), 23–42

[4] M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, K. R. M. Leino, “Boogie: A Modular Reusable Verifier for Object-Oriented Programs”, Formal Methods for Components and Objects, 4th International Symposium, FMCO 2005 (Amsterdam, The Netherlands, November 1–4), Lecture Notes in Computer Science, 4111, Springer, 2006, 364–387 | DOI

[5] E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, S. Tobies, “VCC: A Practical System for Verifying Concurrent C”, Theorem Proving in Higher Order Logics, 22nd International Conference, TPHOLs 2009 (Munich, Germany, August 17–20), Lecture Notes in Computer Science, 5674, Springer, 2009, 23–42 | DOI | MR

[6] J.-C. Filliâtre, C. Marché, “Multi-prover Verification of C Programs”, Formal Methods and Software Engineering, 6th International Conference on Formal Engineering Methods, ICFEM 2004 (Seattle, WA, USA, November 8–12), Lecture Notes in Computer Science, 3308, Springer, 2004, 15–29 | DOI

[7] K. Rustan M. Leino, “Automating Induction with an SMT Solver”, Verification, Model Checking, and Abstract Interpretation, 13th International Conference, VMCAI 2012 (Philadelphia, PA, USA, January 22–24), Lecture Notes in Computer Science, 7148, Springer, 2012, 315–331 | DOI | MR | Zbl

[8] K. Rustan M. Leino, “Dafny: An Automatic Program Verifier for Functional Correctness”, Logic for Programming, Artificial Intelligence, and Reasoning, 16th International Conference, LPAR-16 (Dakar, Senegal, April 25–May 1), Lecture Notes in Computer Science, 6355, Springer, 2010, 348–370 | DOI | MR | Zbl

[9] X. Leroy, “Formal Verification of a Realistic Compiler”, Communications of the ACM, 52:7 (2009), 107–115 | DOI

[10] I. V. Maryasov, The Mixed Axiomatic Semantics Method, Preprint No 160, Siberian Division of the Russian Academy of Sciences, A. P. Ershov Institute of Informatics Systems, Novosibirsk, 2011 http://www.iis.nsk.su/files/preprints/160.pdf

[11] 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

[12] L. de Moura, N. Bjørner, “Z3: An Efficient SMT Solver”, Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008 (Budapest, Hungary, March 29–April 6), Lecture Notes in Computer Science, 4963, Springer, 2008, 337–340 | DOI

[13] V. A. Nepomniaschy, “Symbolic Verification Method for Definite Iteration over Altered Data Structures”, Programming and Computer Software, 1 (2005), 1–12 | DOI | MR

[14] V. A. Nepomniaschy, “Verification of Definite Iteration over Hierarchical Data structures”, Fundamental Approaches to Software Engineering, Second International Conference, FASE'99 (Amsterdam, The Netherlands, March 22–28), Lecture Notes in Computer Science, 1577, Springer, 1999, 176–187 | DOI

[15] V. A. Nepomniaschy, “Verification of Definite Iteration over Tuples of Data Structures”, Programming and Computer Software, 1 (2002), 1–10 | DOI

[16] V. A. Nepomniaschy, I. S. Anureev, M. M. Atuchin, I. V. Maryasov, A. A. Petrov, A. V. Promsky, “C Program Verification in SPECTRUM Multilanguage System”, Automatic Control and Computer Sciences, 45:7 (2011), 413–420 | DOI

[17] V. A. Nepomniaschy, I. S. Anureev, I. N. Mikhaylov, A. V. Promsky, Towards The Verification of C Programs. Part 3. Translation From C-light To C-light-kernel and Its Formal Proof, Preprint, No 97, Siberian Division of the Russian Academy of Sciences, A. P. Ershov Institute of Informatics Systems, Novosibirsk, 2002 (Russian) http://www.iis.nsk.su/files/preprints/097.pdf

[18] V. A. Nepomniaschy, I. S. Anureev, A. V. Promsky, “Towards Verification of C Programs. C-light Language and Its Formal Semantics”, Programming and Computer Software, 28 (2002), 314–323 | DOI | MR | Zbl

[19] V. A. Nepomniaschy, I. S. Anureev, A. V. Promsky, “Towards Verification of C Programs. Axiomatic Semantics of The C-kernel Language”, Programming and Computer Software, 29 (2003), 338–350 | DOI | MR | Zbl

[20] V. A. Nepomniaschy, I. S. Anureev, A. V. Promsky, “Verification-Oriented Language C-Light and Its Structural Operational Semantics”, Perspectives of System Informatics, 5th International Andrei Ershov Memorial Conference, PSI 2003 (Akademgorodok, Novosibirsk, Russia, July 9–12), Lecture Notes in Computer Science, 2890, Springer, 2003, 103–111 | DOI