The complex approach of the C-lightVer system to the automated error localization in C-programs

D. A. Kondratyev ; A. V. Promsky

Modelirovanie i analiz informacionnyh sistem, Tome 26 (2019) no. 4, pp. 502-519.

Résumé

The C-lightVer system for the deductive verification of C programs is being developed at the IIS SB RAS. Based on the two-level architecture of the system, the C-light input language is translated into the intermediate C-kernel language. The meta generator of the correctness conditions receives the C-kernel program and Hoare logic for the C-kernel as input. To solve the well-known problem of determining loop invariants, the definite iteration approach was chosen. The body of the definite iteration loop is executed once for each element of the finite dimensional data structure, and the inference rule for them uses the substitution operation rep, which represents the action of the cycle in symbolic form. Also, in our meta generator, the method of semantic markup of correctness conditions has been implemented and expanded. It allows to generate explanations for unproven conditions and simplifies the errors localization. Finally, if the theorem prover fails to determine the truth of the condition, we can focus on proving its falsity. Thus a method of proving the falsity of the correctness conditions in the ACL2 system was developed. The need for more detailed explanations of the correctness conditions containing the replacement operation rep has led to a change of the algorithms for generating the replacement operation, and the generation of explanations for unproven correctness conditions. Modifications of these algorithms are presented in the article. They allow marking rep definition with semantic labels, extracting semantic labels from rep definition and generating description of break execution condition.

Détail

Keywords: deductive verification, semantic label, error localization, C-lightVer, MetaVCG, definite iteration, proof strategy.
Mots-clés : ACL2

Bibliographie

[1] De Angelis E., Fioravanti F., Pettorossi A., Proietti M., “Lemma Generation for Horn Clause Satisfiability: A Preliminary Study”, VPT 2019, EPTCS, 299, 2019, 4–18 | DOI

[2] Apt K. R., Olderog E.-R., “Fifty years of Hoare's logic”, Formal Aspects of Computing, 31:6 (2019), 751-807 | DOI | MR | Zbl

[3] Blanchard A., Loulergue F., Kosmatov N., “Towards Full Proof Automation in Frama-C Using Auto-active Verification”, NFM 2019, LNCS, 11460, 2019, 88–105

[4] De Carvalho D. et al., “Teaching Programming and Design-by-Contract”, ICL 2018, AISC, 916, 2019, 68–76

[5] Denney E., Fischer B., “Explaining Verification Conditions”, AMAST 2008, LNCS, 5140, 2008, 145–159 | Zbl

[6] Efremov D., Mandrykin M., Khoroshilov A., “Deductive Verification of Unmodified Linux Kernel Library Functions”, ISoLA 2018, LNCS, 11245, 2018, 216–234

[7] Fraer R., “Tracing the Origins of Verification Conditions”, AMAST 1996, LNCS, 1101, 1996, 241–255 | MR

[8] Galeotti J. P., Furia C. A., May E., Fraser G., Zeller A., “Inferring Loop Invariants by Mutation, Dynamic Analysis, and Static Checking”, IEEE Transactions on Software Engineering, 41:10 (2015), 1019–1037 | DOI

[9] Hähnle R., Huisman M., “Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools”, Computing and Software Science, LNCS, 10000, 2019, 345–373

[10] Heras J., Komendantskaya E., Johansson M., Maclean E., “Proof-Pattern Recognition and Lemma Discovery in ACL2”, LPAR 2013, LNCS, 8312, 2013, 389–406 | MR | Zbl

[11] Johansson M., “Lemma Discovery for Induction”, CICM 2019, LNCS, 11617, 2019, 125–139 | Zbl

[12] Khazeev M., Mazzara M., De Carvalho D., Aslam H., Towards A Broader Acceptance of Formal Verification Tools: The Role of Education, 2019, arXiv: 1906.01430 [cs.SE]

[13] Kondratyev D. A., Automated Error Localization in C Programs, bitbucket.org/Kondratyev/verify-c-light

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

[15] Kondratyev D. A., Maryasov I. V., Nepomniaschy V. A., “The Automation of C Program Verification by Symbolic Method of Loop Invariants Elimination”, Modeling and Analysis of Information Systems, 25:5 (2018), 491–505 (in Russian) | MR

[16] Kondratyev D. A., Promsky A. V., “Developing a Self-Applicable Verification System. Theory and Practice”, Automatic Control and Computer Sciences, 49:7 (2015), 445–452 | DOI

[17] Kondratyev D. A., Promsky A. V., “Towards Automated Error Localization in C Programs with Loops”, System Informatics, 2019, no. 14, 31–44

[18] Kondratyev D., Promsky A., “Proof Strategy for Automated Sisal Program Verification”, TOOLS 2019, LNCS, 11771, 2019, 113-120

[19] Könighofer R., Toegl R., Bloem R., “Automatic Error Localization for Software Using Deductive Verification”, HVC 2014, LNCS, 8855, 2014, 92–98

[20] Kovács L., “Symbolic Computation and Automated Reasoning for Program Analysis”, IFM 2016, LNCS, 9681, 2016, 20–27 | MR

[21] Leino K. R. M., Millstein T., Saxe J. B., “Generating Error Traces from Verification-Condition Counterexamples”, Science of Computer Programming, 55:1–3 (2005), 209–226 | DOI | MR | Zbl

[22] Li J., Sun J., Li L., Loc Le Q., Lin S-W., “Automatic Loop Invariant Generation and Refinement through Selective Sampling”, ASE 2017, 2017, 782–792

[23] Lin Y., Bundy A., Grov G., Maclean E., “Automating Event-B invariant proofs by rippling and proof patching”, Formal Aspects of Computing, 31:1 (2019), 95–129 | DOI | MR | Zbl

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

[25] Moore J. S., “Milestones from the Pure Lisp Theorem Prover to ACL2”, Formal Aspects of Computing, 31:6 (2019), 699–732 | DOI | MR | Zbl

[26] Moriconi M., Schwarts R. L., “Automatic Construction of Verification Condition Generators From Hoare Logics”, ICALP 1981, LNCS, 115, 1981, 363–377 | MR | Zbl

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

[28] Reger G., Voronkov A., “Induction in Saturation-Based Proof Search”, CADE 2019, LNCS, 11716, 2019, 477–494 | MR | Zbl

[29] Srivastava S., Gulwani S., Foster J. S., “Template-Based Program Verification and Program Synthesis”, International Journal on Software Tools for Technology Transfer, 15:5–6 (2013), 497–518 | DOI | MR

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

[31] Volkov G., Mandrykin M., Efremov D., “Lemma Functions for Frama-C: C Programs as Proofs”, 2018 Ivannikov Ispras Open Conference (ISPRAS), 2018, 31–38

[32] Yang W., Fedyukovich G., Gupta A., “Lemma Synthesis for Automating Induction over Algebraic Data Types”, CP 2019, LNCS, 11802, 2019, 600-617