The Complex Approach of the C-lightVer System to the Automated Error Localization in C-programs
https://doi.org/10.18255/1818-1015-2019-4-502-519
Abstract
Keywords
About the Authors
Dmitry A. KondratyevRussian Federation
postgraduate student
Alexei V. Promsky
Russian Federation
PhD
References
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.
2. Apt K. R., Olderog E.-R., “Fifty years of Hoare’s logic”, Formal Aspects of Computing, 31:6 (2019), 751–807.
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.
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.
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.
9. Hahnle 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.
11. Johansson M., “Lemma Discovery for Induction”, CICM 2019, LNCS, 11617, 2019, 125–139.
12. Khazeev M., Mazzara M., De Carvalho D., Aslam H., “Towards A Broader Acceptance of Formal Verification Tools: The Role of Education”, 2019, arXiv:abs/1906.01430.
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).
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.
17. Kondratyev D. A., Promsky A. V., “Towards Automated Error Localization in C Programs with Loops”, System Informatics, 2019, № 14, 31–44.
18. Kondratyev D., Promsky A., “Proof Strategy for Automated Sisal Program Verification”, TOOLS 2019, LNCS, 11771, 2019, 113-120.
19. Konighofer R., Toegl R., Bloem R., “Automatic Error Localization for Software Using Deductive Verification”, HVC 2014, LNCS, 8855, 2014, 92–98.
20. Kovacs L., “Symbolic Computation and Automated Reasoning for Program Analysis”, IFM 2016, LNCS, 9681, 2016, 20–27.
21. Leino K. R. M., Millstein T., Saxe J. B., “Generating Error Traces from VerificationCondition Counterexamples”, Science of Computer Programming, 55:1–3 (2005), 209–226.
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.
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.
25. Moore J. S., “Milestones from the Pure Lisp Theorem Prover to ACL2”, Formal Aspects of Computing, 31:6 (2019), 699–732.
26. Moriconi M., Schwarts R. L., “Automatic Construction of Verification Condition Generators From Hoare Logics”, ICALP 1981, LNCS, 115, 1981, 363–377.
27. Nepomniaschy V. A., “Symbolic Method of Verification of Definite Iterations over Altered Data Structures”, Programming and Computer Software, 31:1 (2005), 1–9.
28. Reger G., Voronkov A., “Induction in Saturation-Based Proof Search”, CADE 2019, LNCS, 11716, 2019, 477–494.
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.
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.
Review
For citations:
Kondratyev D.A., Promsky A.V. The Complex Approach of the C-lightVer System to the Automated Error Localization in C-programs. Modeling and Analysis of Information Systems. 2019;26(4):502-519. (In Russ.) https://doi.org/10.18255/1818-1015-2019-4-502-519