The Complex Approach of the C-lightVer System to the Automated Error Localization in C-programs
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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2019-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1273 |
| _version_ | 1797877892481286144 |
|---|---|
| author | Dmitry A. Kondratyev Alexei V. Promsky |
| author_facet | Dmitry A. Kondratyev Alexei V. Promsky |
| author_sort | Dmitry A. Kondratyev |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-10T02:24:13Z |
| format | Article |
| id | doaj.art-a52b77cbccd142f49b9958d406ff6cce |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:24:13Z |
| publishDate | 2019-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-a52b77cbccd142f49b9958d406ff6cce2023-03-13T08:07:34ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172019-12-0126450251910.18255/1818-1015-2019-4-502-519950The Complex Approach of the C-lightVer System to the Automated Error Localization in C-programsDmitry A. Kondratyev0Alexei V. Promsky1Институт систем информатики им. А. П. Ершова СО РАНИнститут систем информатики им. А. П. Ершова СО РАН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.https://www.mais-journal.ru/jour/article/view/1273дедуктивная верификациясемантическая меткалокализация ошибокc-lightveracl2метагенератор условий корректностифинитная итерациястратегия доказательства |
| spellingShingle | Dmitry A. Kondratyev Alexei V. Promsky The Complex Approach of the C-lightVer System to the Automated Error Localization in C-programs Моделирование и анализ информационных систем дедуктивная верификация семантическая метка локализация ошибок c-lightver acl2 метагенератор условий корректности финитная итерация стратегия доказательства |
| title | The Complex Approach of the C-lightVer System to the Automated Error Localization in C-programs |
| title_full | The Complex Approach of the C-lightVer System to the Automated Error Localization in C-programs |
| title_fullStr | The Complex Approach of the C-lightVer System to the Automated Error Localization in C-programs |
| title_full_unstemmed | The Complex Approach of the C-lightVer System to the Automated Error Localization in C-programs |
| title_short | The Complex Approach of the C-lightVer System to the Automated Error Localization in C-programs |
| title_sort | complex approach of the c lightver system to the automated error localization in c programs |
| topic | дедуктивная верификация семантическая метка локализация ошибок c-lightver acl2 метагенератор условий корректности финитная итерация стратегия доказательства |
| url | https://www.mais-journal.ru/jour/article/view/1273 |
| work_keys_str_mv | AT dmitryakondratyev thecomplexapproachoftheclightversystemtotheautomatederrorlocalizationincprograms AT alexeivpromsky thecomplexapproachoftheclightversystemtotheautomatederrorlocalizationincprograms AT dmitryakondratyev complexapproachoftheclightversystemtotheautomatederrorlocalizationincprograms AT alexeivpromsky complexapproachoftheclightversystemtotheautomatederrorlocalizationincprograms |