The automation of C program verification by symbolic method of loop invariants elimination

D. A. Kondratyev ; I. V. Maryasov ; V. A. Nepomnyaschy

Modelirovanie i analiz informacionnyh sistem, Tome 25 (2018) no. 5, pp. 491-505.

Résumé

During deductive verification of programs written in imperative languages, the generation and proof of verification conditions corresponding to loops can cause difficulties, because each one must be provided with an invariant whose construction is often a challenge. As a rule, the methods of invariant synthesis are heuristic ones. This impedes its application. An alternative is the symbolic method of loop invariant elimination suggested by V.A. Nepomniaschy in 2005. Its idea is to represent a loop body in a form of special replacement operation under certain constraints. This operation expresses loop effect in a symbolic form and allows to introduce an inference rule which uses no invariants in axiomatic semantics. This work represents the further development of this method. It extends the mixed axiomatic semantics method suggested for C-light program verification. This extension includes the verification method of iterations over changeable arrays possibly with loop exit in C-light programs. The method contains the inference rule for iterations without loop invariants. This rule was implemented in verification conditions generator which is a part of the automated system of C-light program verification. To prove verification conditions automatically in ACL2, two algorithms were developed and implemented. The first one automatically generates the replacement operation in ACL2 language, the second one automatically generates auxiliary lemmas which allow to prove the obtained verification conditions in ACL2 successfully in automatic mode. An example which illustrates the application of the mentioned methods is described.

Détail

Keywords: C-light, mixed axiomatic semantics, definite iteration, arrays, specification, verification, Hoare logic.
Mots-clés : loop invariants, ACL2

Bibliographie

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

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

[3] Dongarra J. J., van der Steen A. J., “High-performance computing systems: Status and outlook”, Acta Numerica, 21 (2012), 379–474 | DOI | MR | Zbl

[4] Filliâtre J.-C., Marché C., “Multi-prover Verification of C Programs”, 6th ICFEM, LNCS, 3308, 2004, 15–29

[5] Jacobs B., Kiniry J. L., Warnier M., “Java Program Verification Challenges”, FMCO 2002, LNCS, 2852, 2003, 202–219

[6] Kaufmann M., Moore J. S., “An Industrial Strength Theorem Prover for a Logic Based on Common Lisp”, IEEE Transactions on Software Engineering, 23:4 (1997), 203–213 | DOI | MR

[7] Kondratyev D., “Implementing the Symbolic Method of Verification in the C-Light Project”, PSI 2017, LNCS, 10742, 2018, 227–240

[8] Kondratyev D. A., Towards Loop Invariant Elimination for Definite Iterations over Changeable Data Structures in C Programs Verification. Appendices, https://bitbucket.org/c-light/loop-invariant-elimination

[9] Kondratyev D. A., Maryasov I. V., Nepomniaschy V. A., “Towards Loop Invariant Elimination for Definite Iterations over Changeable Data Structures in C Programs Verification”, PSSV 2018, Workshop Proceedings, Yaroslavl, 2018, 51–57

[10] Li J., Sun J., Li L., Loc Le Q., Lin S-W., “Automatic Loop Invariant Generation and Refinement through Selective Sampling”, 32nd IEEE/ACM International Conference on Automated Software Engineering (ASE), 2017, 782–792

[11] Maryasov I. V., Nepomniaschy V. A., “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

[12] Maryasov I. V., Nepomniaschy V. A., Kondratyev D. A., “Invariant Elimination of Definite Iterations over Arrays in C Programs Verification”, Modeling and Analysis of Information Systems, 24:6 (2017), 743–754 | DOI | MR

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

[14] Nepomniaschy V. A., “Symbolic Method of Verification of Definite Iterations over Altered Data Structures”, Programming and Computer Software, 31:1 (2005), 1–9 | DOI | MR | Zbl

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