maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2019-4-502-519mais-1273Research ArticleComputing Methodologies and ApplicationsКомплексный подход системы C-lightVer к автоматизированной локализации ошибок в C-программахThe Complex Approach of the C-lightVer System to the Automated Error Localization in C-programshttps://orcid.org/0000-0002-9387-6735КондратьевДмитрий АлександровичKondratyevDmitry A.

аспирант

postgraduate student

apple-66@mail.ruhttps://orcid.org/0000-0002-5963-2390ПромскийАлексей ВладимировичPromskyAlexei V.

канд. физ.-мат. наук

PhD

promsky@iis.nsk.suИнститут систем информатики им. А. П. Ершова СО РАНРоссияA. P. Ershov Institute of Informatics Systems SB RASRussian Federation201913122019264502519Copyright © Кондратьев Д.А., Промский А.В., 20192019Кондратьев Д.А., Промский А.В.Kondratyev D.A., Promsky A.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1273

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

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.

дедуктивная верификациясемантическая меткалокализация ошибокC-lightVerACL2метагенератор условий корректностифинитная итерациястратегия доказательстваdeductive verificationsemantic labelerror localizationC-lightVerACL2MetaVCGdefinite iterationproof strategyИсследование выполнено при частичной финансовой поддержке РФФИ в рамках научного проекта № 17-01-00789.This work was partially funded by the RFBR according to the research № 17-01-00789.ReferencesDe Angelis E., Fioravanti F., Pettorossi A., Proietti M., “Lemma Generation for Horn Clause Satisfiability: A Preliminary Study”, VPT 2019, EPTCS, 299, 2019, 4–18.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.Apt K. R., Olderog E.-R., “Fifty years of Hoare’s logic”, Formal Aspects of Computing, 31:6 (2019), 751–807.Apt K. R., Olderog E.-R., “Fifty years of Hoare’s logic”, Formal Aspects of Computing, 31:6 (2019), 751–807.Blanchard A., Loulergue F., Kosmatov N., “Towards Full Proof Automation in Frama-C Using Auto-active Verification”, NFM 2019, LNCS, 11460, 2019, 88–105.Blanchard A., Loulergue F., Kosmatov N., “Towards Full Proof Automation in Frama-C Using Auto-active Verification”, NFM 2019, LNCS, 11460, 2019, 88–105.De Carvalho D. et al., “Teaching Programming and Design-by-Contract”, ICL 2018, AISC, 916, 2019, 68–76.De Carvalho D. et al., “Teaching Programming and Design-by-Contract”, ICL 2018, AISC, 916, 2019, 68–76.Denney E., Fischer B., “Explaining Verification Conditions”, AMAST 2008, LNCS, 5140, 2008, 145–159.Denney E., Fischer B., “Explaining Verification Conditions”, AMAST 2008, LNCS, 5140, 2008, 145–159.Efremov D., Mandrykin M., Khoroshilov A., “Deductive Verification of Unmodified Linux Kernel Library Functions”, ISoLA 2018, LNCS, 11245, 2018, 216–234.Efremov D., Mandrykin M., Khoroshilov A., “Deductive Verification of Unmodified Linux Kernel Library Functions”, ISoLA 2018, LNCS, 11245, 2018, 216–234.Fraer R., “Tracing the Origins of Verification Conditions”, AMAST 1996, LNCS, 1101, 1996, 241–255.Fraer R., “Tracing the Origins of Verification Conditions”, AMAST 1996, LNCS, 1101, 1996, 241–255.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.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.Hahnle R., Huisman M., “Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools”, Computing and Software Science, LNCS, 10000, 2019, 345–373.Hahnle R., Huisman M., “Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools”, Computing and Software Science, LNCS, 10000, 2019, 345–373.Heras J., Komendantskaya E., Johansson M., Maclean E., “Proof-Pattern Recognition and Lemma Discovery in ACL2”, LPAR 2013, LNCS, 8312, 2013, 389–406.Heras J., Komendantskaya E., Johansson M., Maclean E., “Proof-Pattern Recognition and Lemma Discovery in ACL2”, LPAR 2013, LNCS, 8312, 2013, 389–406.Johansson M., “Lemma Discovery for Induction”, CICM 2019, LNCS, 11617, 2019, 125–139.Johansson M., “Lemma Discovery for Induction”, CICM 2019, LNCS, 11617, 2019, 125–139.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.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.Kondratyev D. A., “Automated Error Localization in C Programs.”, bitbucket.org/Kondratyev/verify-c-light.Kondratyev D. A., “Automated Error Localization in C Programs.”, bitbucket.org/Kondratyev/verify-c-light.Kondratyev D., “Implementing the Symbolic Method of Verification in the C-Light Project”, PSI 2017, LNCS, 10742, 2018, 227–240.Kondratyev D., “Implementing the Symbolic Method of Verification in the C-Light Project”, PSI 2017, LNCS, 10742, 2018, 227–240.Кондратьев Д. А., Марьясов И. В., Непомнящий В. А., “Автоматизация верификации C-программ с использованием символического метода элиминации инвариантов циклов”, Моделирование и анализ информационных систем, 25:5 (2018), 491–505;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).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.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.Kondratyev D. A., Promsky A. V., “Towards Automated Error Localization in C Programs with Loops”, System Informatics, 2019, № 14, 31–44.Kondratyev D. A., Promsky A. V., “Towards Automated Error Localization in C Programs with Loops”, System Informatics, 2019, № 14, 31–44.Kondratyev D., Promsky A., “Proof Strategy for Automated Sisal Program Verification”, TOOLS 2019, LNCS, 11771, 2019, 113-120.Kondratyev D., Promsky A., “Proof Strategy for Automated Sisal Program Verification”, TOOLS 2019, LNCS, 11771, 2019, 113-120.Konighofer R., Toegl R., Bloem R., “Automatic Error Localization for Software Using Deductive Verification”, HVC 2014, LNCS, 8855, 2014, 92–98.Konighofer R., Toegl R., Bloem R., “Automatic Error Localization for Software Using Deductive Verification”, HVC 2014, LNCS, 8855, 2014, 92–98.Kov´acs L., “Symbolic Computation and Automated Reasoning for Program Analysis”, IFM 2016, LNCS, 9681, 2016, 20–27.Kovacs L., “Symbolic Computation and Automated Reasoning for Program Analysis”, IFM 2016, LNCS, 9681, 2016, 20–27.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.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.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.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.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.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.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.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.Moore J. S., “Milestones from the Pure Lisp Theorem Prover to ACL2”, Formal Aspects of Computing, 31:6 (2019), 699–732.Moore J. S., “Milestones from the Pure Lisp Theorem Prover to ACL2”, Formal Aspects of Computing, 31:6 (2019), 699–732.Moriconi M., Schwarts R. L., “Automatic Construction of Verification Condition Generators From Hoare Logics”, ICALP 1981, LNCS, 115, 1981, 363–377.Moriconi M., Schwarts R. L., “Automatic Construction of Verification Condition Generators From Hoare Logics”, ICALP 1981, LNCS, 115, 1981, 363–377.Nepomniaschy V. A., “Symbolic Method of Verification of Definite Iterations over Altered Data Structures”, Programming and Computer Software, 31:1 (2005), 1–9.Nepomniaschy V. A., “Symbolic Method of Verification of Definite Iterations over Altered Data Structures”, Programming and Computer Software, 31:1 (2005), 1–9.Reger G., Voronkov A., “Induction in Saturation-Based Proof Search”, CADE 2019, LNCS, 11716, 2019, 477–494.Reger G., Voronkov A., “Induction in Saturation-Based Proof Search”, CADE 2019, LNCS, 11716, 2019, 477–494.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.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.Tuerk T., “Local Reasoning about While-Loops”, VSTTE 2010. Workshop Proceedings, 2010, 29–39.Tuerk T., “Local Reasoning about While-Loops”, VSTTE 2010. Workshop Proceedings, 2010, 29–39.Volkov G., Mandrykin M., Efremov D., “Lemma Functions for Frama-C: C Programs as Proofs”, 2018 Ivannikov Ispras Open Conference (ISPRAS), 2018, 31–38.Volkov G., Mandrykin M., Efremov D., “Lemma Functions for Frama-C: C Programs as Proofs”, 2018 Ivannikov Ispras Open Conference (ISPRAS), 2018, 31–38.Yang W., Fedyukovich G., Gupta A., “Lemma Synthesis for Automating Induction over Algebraic Data Types”, CP 2019, LNCS, 11802, 2019, 600-617.Yang W., Fedyukovich G., Gupta A., “Lemma Synthesis for Automating Induction over Algebraic Data Types”, CP 2019, LNCS, 11802, 2019, 600-617.

The authors declare that there are no conflicts of interest present.