Automatic C Program Verification Based on Mixed Axiomatic Semantics
<p>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...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2013-01-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | http://mais-journal.ru/jour/article/view/157 |
| _version_ | 1797964997435850752 |
|---|---|
| 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 | <p>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.</p> |
| first_indexed | 2024-04-11T01:52:16Z |
| format | Article |
| id | doaj.art-a6f3bfddfe8144d49fd26dee06855029 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-11T01:52:16Z |
| publishDate | 2013-01-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-a6f3bfddfe8144d49fd26dee068550292023-01-03T06:07:44ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172013-01-012065263151Automatic C Program Verification Based on Mixed Axiomatic SemanticsI. V. Maryasov0V. A. Nepomnyaschy1A. V. Promsky2D. A. Kondratyev3Институт систем информатики им. А. П. Ершова СО РАНИнститут систем информатики им. А. П. Ершова СО РАН; Новосибирский государственный университетИнститут систем информатики им. А. П. Ершова СО РАН,Новосибирский государственный университет<p>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.</p>http://mais-journal.ru/jour/article/view/157верификацияоперационная семантикааксиоматическая семантикаязык Cязык C-lightязык C-kernelчастичная корректностьACSLLLVMSimplify |
| spellingShingle | I. V. Maryasov V. A. Nepomnyaschy A. V. Promsky D. A. Kondratyev Automatic C Program Verification Based on Mixed Axiomatic Semantics Моделирование и анализ информационных систем верификация операционная семантика аксиоматическая семантика язык C язык C-light язык C-kernel частичная корректность 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 | верификация операционная семантика аксиоматическая семантика язык C язык C-light язык C-kernel частичная корректность ACSL LLVM Simplify |
| url | http://mais-journal.ru/jour/article/view/157 |
| work_keys_str_mv | AT ivmaryasov automaticcprogramverificationbasedonmixedaxiomaticsemantics AT vanepomnyaschy automaticcprogramverificationbasedonmixedaxiomaticsemantics AT avpromsky automaticcprogramverificationbasedonmixedaxiomaticsemantics AT dakondratyev automaticcprogramverificationbasedonmixedaxiomaticsemantics |