Комплексный подход системы C-lightVer к автоматизированной локализации ошибок в C-программах
https://doi.org/10.18255/1818-1015-2019-4-502-519
Аннотация
Ключевые слова
Об авторах
Дмитрий Александрович КондратьевРоссия
аспирант
Алексей Владимирович Промский
Россия
канд. физ.-мат. наук
Список литературы
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. Кондратьев Д. А., Марьясов И. В., Непомнящий В. А., “Автоматизация верификации C-программ с использованием символического метода элиминации инвариантов циклов”, Моделирование и анализ информационных систем, 25:5 (2018), 491–505;
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. Kov´acs 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.
Рецензия
Для цитирования:
Кондратьев Д.А., Промский А.В. Комплексный подход системы C-lightVer к автоматизированной локализации ошибок в C-программах. Моделирование и анализ информационных систем. 2019;26(4):502-519. https://doi.org/10.18255/1818-1015-2019-4-502-519
For citation:
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