The Automation of C Program Verification by Symbolic Method of Loop Invariants Elimination
During deductive verification of programs written in imperative languages, the generation and proof of verification conditions corresponding to loops can cause difficulties, because each one must be provided with an invariant whose construction is often a challenge. As a rule, the methods of invaria...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2018-10-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/745 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849338861938802688 |
|---|---|
| author | Dmitry Kondratyev Ilya Maryasov Valery Nepomniaschy |
| author_facet | Dmitry Kondratyev Ilya Maryasov Valery Nepomniaschy |
| author_sort | Dmitry Kondratyev |
| collection | DOAJ |
| description | During deductive verification of programs written in imperative languages, the generation and proof of verification conditions corresponding to loops can cause difficulties, because each one must be provided with an invariant whose construction is often a challenge. As a rule, the methods of invariant synthesis are heuristic ones. This impedes its application. An alternative is the symbolic method of loop invariant elimination suggested by V.A. Nepomniaschy in 2005. Its idea is to represent a loop body in a form of special replacement operation under certain constraints. This operation expresses loop effect in a symbolic form and allows to introduce an inference rule which uses no invariants in axiomatic semantics. This work represents the further development of this method. It extends the mixed axiomatic semantics method suggested for C-light program verification. This extension includes the verification method of iterations over changeable arrays possibly with loop exit in C-light programs. The method contains the inference rule for iterations without loop invariants. This rule was implemented in verification conditions generator which is a part of the automated system of C-light program verification. To prove verification conditions automatically in ACL2, two algorithms were developed and implemented. The first one automatically generates the replacement operation in ACL2 language, the second one automatically generates auxiliary lemmas which allow to prove the obtained verification conditions in ACL2 successfully in automatic mode. An example which illustrates the application of the mentioned methods is described. |
| format | Article |
| id | doaj-art-be655fa22ef4441cb8bfc7b210c6c324 |
| institution | Kabale University |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2018-10-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-be655fa22ef4441cb8bfc7b210c6c3242025-08-20T03:44:17ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172018-10-0125549150510.18255/1818-1015-2018-5-491-505521The Automation of C Program Verification by Symbolic Method of Loop Invariants EliminationDmitry Kondratyev0Ilya Maryasov1Valery Nepomniaschy2A.P. Ershov Institute of Informatics Systems SB RAS.A.P. Ershov Institute of Informatics Systems SB RAS.A.P. Ershov Institute of Informatics Systems SB RASDuring deductive verification of programs written in imperative languages, the generation and proof of verification conditions corresponding to loops can cause difficulties, because each one must be provided with an invariant whose construction is often a challenge. As a rule, the methods of invariant synthesis are heuristic ones. This impedes its application. An alternative is the symbolic method of loop invariant elimination suggested by V.A. Nepomniaschy in 2005. Its idea is to represent a loop body in a form of special replacement operation under certain constraints. This operation expresses loop effect in a symbolic form and allows to introduce an inference rule which uses no invariants in axiomatic semantics. This work represents the further development of this method. It extends the mixed axiomatic semantics method suggested for C-light program verification. This extension includes the verification method of iterations over changeable arrays possibly with loop exit in C-light programs. The method contains the inference rule for iterations without loop invariants. This rule was implemented in verification conditions generator which is a part of the automated system of C-light program verification. To prove verification conditions automatically in ACL2, two algorithms were developed and implemented. The first one automatically generates the replacement operation in ACL2 language, the second one automatically generates auxiliary lemmas which allow to prove the obtained verification conditions in ACL2 successfully in automatic mode. An example which illustrates the application of the mentioned methods is described.https://www.mais-journal.ru/jour/article/view/745c-light, loop invariants, mixed axiomatic semantics, definite iteration, arrays, acl2, specification, verification, hoare logic |
| spellingShingle | Dmitry Kondratyev Ilya Maryasov Valery Nepomniaschy The Automation of C Program Verification by Symbolic Method of Loop Invariants Elimination Моделирование и анализ информационных систем c-light, loop invariants, mixed axiomatic semantics, definite iteration, arrays, acl2, specification, verification, hoare logic |
| title | The Automation of C Program Verification by Symbolic Method of Loop Invariants Elimination |
| title_full | The Automation of C Program Verification by Symbolic Method of Loop Invariants Elimination |
| title_fullStr | The Automation of C Program Verification by Symbolic Method of Loop Invariants Elimination |
| title_full_unstemmed | The Automation of C Program Verification by Symbolic Method of Loop Invariants Elimination |
| title_short | The Automation of C Program Verification by Symbolic Method of Loop Invariants Elimination |
| title_sort | automation of c program verification by symbolic method of loop invariants elimination |
| topic | c-light, loop invariants, mixed axiomatic semantics, definite iteration, arrays, acl2, specification, verification, hoare logic |
| url | https://www.mais-journal.ru/jour/article/view/745 |
| work_keys_str_mv | AT dmitrykondratyev theautomationofcprogramverificationbysymbolicmethodofloopinvariantselimination AT ilyamaryasov theautomationofcprogramverificationbysymbolicmethodofloopinvariantselimination AT valerynepomniaschy theautomationofcprogramverificationbysymbolicmethodofloopinvariantselimination AT dmitrykondratyev automationofcprogramverificationbysymbolicmethodofloopinvariantselimination AT ilyamaryasov automationofcprogramverificationbysymbolicmethodofloopinvariantselimination AT valerynepomniaschy automationofcprogramverificationbysymbolicmethodofloopinvariantselimination |