Towards Verification of C Programs: Axiomatic Semantics of the C-kernel Language
| Autor: | A. V. Promskii, Valery A. Nepomniaschy, Igor S. Anureev |
|---|---|
| Rok vydání: | 2003 |
| Předmět: |
Soundness
Theoretical computer science Computer science Programming language Formal semantics (linguistics) computer.software_genre Operational semantics Axiomatic semantics Action semantics TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES Denotational semantics Well-founded semantics TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS Computer Science::Logic in Computer Science Computational semantics Computer Science::Programming Languages computer Software |
| Zdroj: | Programming and Computer Software. 29:338-350 |
| ISSN: | 0361-7688 |
| Popis: | With the aim of the verification of programs in the C-light language l1r, its kernel C-kernel is separated, and an axiomatic semantics for it is suggested. A theorem on soundness of the axiomatic semantics of C-kernel with respect to its operational semantics is proved. The C-light language is used as an input language of the program verification system, which includes a translator to C-kernel and a generator of the correctness conditions for C-kernel programs, which is based on its axiomatic semantics. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full text from SpringerLink