Комплексный подход системы C-lightVer к автоматизированной локализации ошибок в C-программах

В ИСИ СО РАН разрабатывается система C-lightVer для дедуктивной верификации С-программ. Исходя из двухуровневой архитектуры системы, входной язык C-light транслируется в промежуточный язык C-kernel. Метагенератор условий корректности принимает на вход C-kernel программу и логику Хоара для C-kernel. Для решения известной проблемы задания инвариантов циклов выбран подход финитных итераций. Тело цикла финитной итерации исполняется один раз для каждого элемента структуры данных конечной размерности, а правило вывода для них использует операцию замены rep, выражающую действие цикла в символической форме. Также в нашем метагенераторе внедрен и расширен метод семантической разметки условий корректности. Он позволяет порождать пояснения для недоказанных условий и упрощает локализацию ошибок. Наконец, если система ACL2 не справляется с установлением истинности условия, можно сосредоточиться на доказательстве его ложности. Ранее нами был разработан способ доказательства ложности условий корректности для системы ACL2. Необходимость в более подробных объяснениях условий корректности, содержащих операцию замены rep, привела к изменению алгоритмов генерации операции замены, извлечения семантических меток и генерации объяснений недоказанных условий корректности. В статье представлены модификации данных алгоритмов. Эти изменения позволяют пометить исходный код функции rep семантическими метками, извлекать семантические метки из определения rep, а также генерировать описание условия исполнения инструкции break.

дедуктивная верификация, семантическая метка, локализация ошибок, C-lightVer, ACL2, метагенератор условий корректности, финитная итерация, стратегия доказательства

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.