Invariant Elimination of Definite Iterations over Arrays in C Programs Verification

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.

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.

2. C. Barrett, C. L., Conway, M. Deters, L. Hadarean, D. Jovanovi´c, T. King, A. Reynolds, C. Tinelli, “CVC4”, 23rd Int. Conf. CAV, Lecture Notes in Computer Science, 6806 (2011), 171–177.

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.

4. J.-C. Filli˄atre, C. March´e, “Multi-prover Verification of C Programs”, 6th ICFEM, Lecture Notes in Computer Science, 3308 (2004), 15–29.

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.

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.

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, š 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.

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.

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

12. A. Reynolds, V. Kuncak, “Induction for SMT solvers”, 16th Int. Conf. VMCAI, Lecture Notes in Computer Science, 8931 (2015), 80–98.

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