Skip to main content
SpringerLink
Log in

The Complex Approach of the C-lightVer System to the Automated Error Localization in C-Programs

  • Published:
Automatic Control and Computer Sciences Aims and scope Submit manuscript

Abstract—

The C-lightVer system for the deductive verification of C-programs is developed at the A.P. Ershov Institute of Informatics Systems of the Siberian Branch of the Russian Academy of Sciences. The C-light input language is translated into the intermediate C-kernel language based on the two-level architecture of the system. The C-kernel program and Hoare logic for the C-kernel are the input of the metagenerator. The definite iteration approach is used to solve the well-known problem of defining loop invariants. The body of a definite iteration loop is executed once for each element of the finite dimensional data structure, and the inference rule for them uses the replacement operation rep, which represents the action of the loop in a symbolic form. Also, the method of semantic labeling of verification conditions is implemented and extended in our metagenerator. This makes it possible to generate explanations for unproven conditions and simplifies error localization. Finally, if the ACL2 system fails to prove a verification condition, it is possible to focus on proving that it is false. Previously, we developed a method for checking the falsity of verification conditions for the ACL2 system. The need for more detailed explanations of the verification conditions containing the replacement operation rep has led to changes in the algorithms for generating the replacement operation, extracting semantic labels, and generating explanations for unproven verification conditions. The article presents modifications of these algorithms. These modifications make it possible to mark the source code of the rep function with semantic labels, extract semantic labels from the rep definition, and generate a description of the break statement execution condition.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

REFERENCES

  1. De Angelis, E., Fioravanti, F., Pettorossi, A., and Proietti, M., Lemma generation for Horn clause satisfiability: A preliminary study, Electron. Proc. Theor. Comput. Sci., 2019, vol. 299, pp. 4–18.

    Article  Google Scholar 

  2. Apt, K.R. and Olderog, E.-R., Fifty years of Hoare’s logic, Formal Aspects Comput., 2019, vol. 31, no. 6, pp. 751–807.

    Article  MathSciNet  Google Scholar 

  3. Blanchard, A., Loulergue, F., and Kosmatov, N., Towards full proof automation in Frama-C using auto-active verification, Lect. Notes Comput. Sci., 2019, vol. 11460, pp. 88–105.

    Article  Google Scholar 

  4. De Carvalho, D., et al., Teaching programming and design-by-contract, ICL 2018, 2019, pp. 68–76.

    Google Scholar 

  5. Denney, E. and Fischer, B., Explaining verification conditions, AMAST 2008; Lect. Notes Comput. Sci., 2008, vol. 5140, pp. 145–159.

    Article  Google Scholar 

  6. Efremov, D., Mandrykin, M., and Khoroshilov, A., Deductive verification of unmodified Linux kernel library functions, ISoLA 2018; Lect. Notes Comput. Sci., 2018, vol. 11245, pp. 216–234.

    Article  Google Scholar 

  7. Fraer, R., Tracing the Origins of Verification Conditions, Lect. Notes Comput. Sci., 1996 1101, pp. 241–255.

    Article  MathSciNet  Google Scholar 

  8. Galeotti, J.P., Furia, C.A., May, E., Fraser, G., and Zeller, A., Inferring loop invariants by mutation, dynamic analysis, and static checking, IEEE Trans. Software Eng., 2015, vol. 41, no. 10, pp. 1019–1037.

    Article  Google Scholar 

  9. Hähnle, R. and Huisman, M., Deductive software verification: From pen-and-paper proofs to industrial tools, Lect. Notes Comput. Sci., 2019, vol. 10000, pp. 345–373.

    Article  Google Scholar 

  10. Heras, J., Komendantskaya, E., Johansson, M., and Maclean, E., Proof-pattern recognition and lemma discovery in ACL2, LPAR 2013; Lect. Notes Comput. Sci., 2013, vol. 8312, pp. 389–406.

    Article  Google Scholar 

  11. Johansson, M., Lemma discovery for induction, Lect. Notes Comput. Sci., 2019, vol. 11617, pp. 125–139.

    Article  Google Scholar 

  12. Khazeev, M., Mazzara, M., Aslam, H., and de Carvalho, D., Towards a broader acceptance of formal verification tools, ICL 2019: The Impact of the 4th Industrial Revolution on Engineering Education, 2020, pp. 188–200.https://doi.org/10.1007/978-3-030-40271-6_20

  13. Kondratyev, D.A., Automated error localization in C programs. https://www.bitbucket.org/Kondratyev/verify-c-light.

  14. Kondratyev, D.A., Implementing the symbolic method of verification in the C-light project, Lect. Notes Comput. Sci., 2018, vol. 10742, pp. 227–240.

    Article  Google Scholar 

  15. Kondratyev, D.A., Maryasov, I.V., and Nepomniaschy, V.A., The automation of C program verification by the symbolic method of loop invariant elimination, Model. Anal. Inf. Sist., 2018, vol. 25, no. 5, pp. 491–505.

    Article  MathSciNet  Google Scholar 

  16. Kondratyev, D.A. and Promsky, A.V., Developing a self-applicable verification system. Theory and practice, Autom. Control Comput. Sci., 2015, vol. 49, no. 7, pp. 445–452.

    Article  Google Scholar 

  17. Kondratyev, D.A. and Promsky, A.V., Towards automated error localization in C programs with loops, Syst. Inf., 2019, no. 14, pp. 31–44.

  18. Kondratyev, D. and Promsky, A., Proof strategy for automated Sisal program verification, TOOLS 2019; Lect. Notes Comput. Sci., 2019, vol. 11771, pp. 113–120.

    Article  Google Scholar 

  19. Könighofer, R., Toegl, R., and Bloem, R., Automatic error localization for software using deductive verification, Lect. Notes Comput. Sci., 2014, vol. 8855, pp. 92–98.

    Article  Google Scholar 

  20. Kovács, L., Symbolic computation and automated reasoning for program analysis, Lect. Notes Comput. Sci., 2016, vol. 9681, pp. 20–27.

    Article  MathSciNet  Google Scholar 

  21. Leino, K.R.M., Millstein, T., and Saxe, J.B., Generating error traces from verification-condition counterexamples, Sci. Comput. Program., 2005, vol. 55, nos. 1–3, pp. 209–226.

    Article  MathSciNet  Google Scholar 

  22. Li, J., Sun, J., Li, L., Loc Le, Q., and Lin, S.-W., Automatic loop invariant generation and refinement through selective sampling, ASE 2017, 2017, pp. 782–792.

  23. Lin, Y., Bundy, A., Grov, G., and Maclean, E., Automating Event-B invariant proofs by rippling and proof patching, Formal Aspects Comput., 2019, vol. 31, no. 1, pp. 95–129.

    Article  MathSciNet  Google Scholar 

  24. Maryasov, I.V., Nepomniaschy, V.A., Promsky, A.V., and Kondratyev, D.A., Automatic C program verification based on mixed axiomatic semantics, Autom. Control Comput. Sci., 2014, vol. 48, no. 7, pp. 407–414.

    Article  Google Scholar 

  25. Moore, J.S., Milestones from the pure lisp theorem prover to ACL2, Formal Aspects Comput., 2019, vol. 31, no. 6, pp. 699–732.

    Article  MathSciNet  Google Scholar 

  26. Moriconi, M. and Schwarts, R.L., Automatic construction of verification condition generators from Hoare logics, Lect. Notes Comput. Sci., 1981, vol. 115, pp. 363–377.

    Article  MathSciNet  Google Scholar 

  27. Nepomniaschy, V.A., Symbolic method of verification of definite iterations over altered data structures, Program. Comput. Software, 2005, vol. 31, no. 1, pp. 1–9.

    Article  MathSciNet  Google Scholar 

  28. Reger, G. and Voronkov, A., Induction in saturation-based proof search, Lect. Notes Comput. Sci., 2019, vol. 11716, pp. 477–494.

    Article  MathSciNet  Google Scholar 

  29. Srivastava, S., Gulwani, S., and Foster, J.S., Template-based program verification and program synthesis, Int. J. Software Tools Technol. Transfer, 2013, vol. 15, nos. 5–6, pp. 497–518.

    Article  Google Scholar 

  30. Tuerk, T., Local reasoning about while-loops, VSTTE 2010, Workshop Proceedings, 2010, pp. 29–39.

  31. Volkov, G., Mandrykin, M., and Efremov, D., Lemma functions for Frama-C: C programs as proofs, 2018 Ivannikov ISP RAS Open Conference, 2018, pp. 31–38.

  32. Yang, W., Fedyukovich, G., and Gupta, A., Lemma synthesis for automating induction over algebraic data types, Lect. Notes Comput. Sci., 2019, vol. 11 802, pp. 600–617.

    Article  Google Scholar 

Download references

Funding

This work was supported in part by the Russian Foundation for Basic Research, project no. 17-01-00789.

Author information

Authors and Affiliations

  1. Ershov Institute of Informatics Systems, Siberian Branch, Russian Academy of Sciences, 630090, Novosibirsk, Russia

    D. A. Kondratyev & A. V. Promsky

Authors
  1. D. A. Kondratyev
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. A. V. Promsky
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to D. A. Kondratyev or A. V. Promsky.

Ethics declarations

CONFLICT OF INTEREST

The authors declare that they have no conflicts of interest.

ADDITIONAL INFORMATION

Dmitry A. Kondratyev, orcid.org/0000-0002-9387-6735, postgraduate student.

Alexei V. Promsky, orcid.org/0000-0002-5963-2390, PhD.

Additional information

Translated by O. Pismenov

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Kondratyev, D.A., Promsky, A.V. The Complex Approach of the C-lightVer System to the Automated Error Localization in C-Programs. Aut. Control Comp. Sci. 54, 728–739 (2020). https://doi.org/10.3103/S0146411620070093

Download citation

  • Received:

  • Revised:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.3103/S0146411620070093

Keywords:

Search

Navigation