Automatic C Program Verification Based on Mixed Axiomatic Semantics
The development of the C-light project resulted in the application of new formalisms and implementation techniques which facilitate the verification process. The mixed axiomatic semantics proposes a choice between simplified and full-strength deduction rules depending on program objects and their pr...
Saved in:
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2013-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/157 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1850024009733767168 |
|---|---|
| author | I. V. Maryasov V. A. Nepomnyaschy A. V. Promsky D. A. Kondratyev |
| author_facet | I. V. Maryasov V. A. Nepomnyaschy A. V. Promsky D. A. Kondratyev |
| author_sort | I. V. Maryasov |
| collection | DOAJ |
| description | The development of the C-light project resulted in the application of new formalisms and implementation techniques which facilitate the verification process. The mixed axiomatic semantics proposes a choice between simplified and full-strength deduction rules depending on program objects and their properties. The LLVM infrastructure helps greatly in writing the C-light program analyzer and translator. The semantical labeling technique, proposed earlier, can now be safely kept in verification conditions during their proof. Two programs from the well-known verification benchmarks illustrate the applicability of the system. |
| format | Article |
| id | doaj-art-e92111dd8031493f94efc52057156919 |
| institution | DOAJ |
| issn | 1818-1015 2313-5417 |
| language | English |
| publishDate | 2013-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj-art-e92111dd8031493f94efc520571569192025-08-20T03:01:14ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172013-12-01206526310.18255/1818-1015-2013-6-52-63151Automatic C Program Verification Based on Mixed Axiomatic SemanticsI. V. Maryasov0V. A. Nepomnyaschy1A. V. Promsky2D. A. Kondratyev3A.P. Ershov Institute of Informatics Systems SB RASA.P. Ershov Institute of Informatics Systems SB RAS; Novosibirsk State UniversityA.P. Ershov Institute of Informatics Systems SB RASNovosibirsk State UniversityThe development of the C-light project resulted in the application of new formalisms and implementation techniques which facilitate the verification process. The mixed axiomatic semantics proposes a choice between simplified and full-strength deduction rules depending on program objects and their properties. The LLVM infrastructure helps greatly in writing the C-light program analyzer and translator. The semantical labeling technique, proposed earlier, can now be safely kept in verification conditions during their proof. Two programs from the well-known verification benchmarks illustrate the applicability of the system.https://www.mais-journal.ru/jour/article/view/157program verificationoperational semanticsaxiomatic semanticscc-lightc-kernelpartial correctnessacslllvmsimplify |
| spellingShingle | I. V. Maryasov V. A. Nepomnyaschy A. V. Promsky D. A. Kondratyev Automatic C Program Verification Based on Mixed Axiomatic Semantics Моделирование и анализ информационных систем program verification operational semantics axiomatic semantics c c-light c-kernel partial correctness acsl llvm simplify |
| title | Automatic C Program Verification Based on Mixed Axiomatic Semantics |
| title_full | Automatic C Program Verification Based on Mixed Axiomatic Semantics |
| title_fullStr | Automatic C Program Verification Based on Mixed Axiomatic Semantics |
| title_full_unstemmed | Automatic C Program Verification Based on Mixed Axiomatic Semantics |
| title_short | Automatic C Program Verification Based on Mixed Axiomatic Semantics |
| title_sort | automatic c program verification based on mixed axiomatic semantics |
| topic | program verification operational semantics axiomatic semantics c c-light c-kernel partial correctness acsl llvm simplify |
| url | https://www.mais-journal.ru/jour/article/view/157 |
| work_keys_str_mv | AT ivmaryasov automaticcprogramverificationbasedonmixedaxiomaticsemantics AT vanepomnyaschy automaticcprogramverificationbasedonmixedaxiomaticsemantics AT avpromsky automaticcprogramverificationbasedonmixedaxiomaticsemantics AT dakondratyev automaticcprogramverificationbasedonmixedaxiomaticsemantics |