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...
Saved in:
| 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 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849688321198915584 |
|---|---|
| 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. |
| format | Article |
| id | doaj-art-a52b77cbccd142f49b9958d406ff6cce |
| institution | DOAJ |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2019-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-a52b77cbccd142f49b9958d406ff6cce2025-08-20T03:22:03ZengYaroslavl 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. Promsky1A. P. Ershov Institute of Informatics Systems SB RASA. P. Ershov Institute of Informatics Systems SB RASThe 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/1273deductive verificationsemantic labelerror localizationc-lightveracl2metavcgdefinite iterationproof strategy |
| spellingShingle | Dmitry A. Kondratyev Alexei V. Promsky The Complex Approach of the C-lightVer System to the Automated Error Localization in C-programs Моделирование и анализ информационных систем deductive verification semantic label error localization c-lightver acl2 metavcg definite iteration proof strategy |
| 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 | deductive verification semantic label error localization c-lightver acl2 metavcg definite iteration proof strategy |
| 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 |