Attribute Annotations and Their Use in C Program Deductive Verification
In this paper a new kind of annotations, called attribute annotations, and the methodology for their application in a deductive program verification are proposed. A collection of annotating attributes for the subset C-kernel of the C language is described, and on their base two versions of axiomatic...
Saved in:
| Main Authors: | M. M. Atuchin, I. S. Anureev |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2011-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1095 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Similar Items
-
Automatic C Program Verification Based on Mixed Axiomatic Semantics
by: I. V. Maryasov, et al.
Published: (2013-12-01) -
Deductive Verification of Telecommunication Systems Written in C
by: I. S. Anureev
Published: (2015-03-01) -
C Program Verification: VC Explanation and the Standard Library
by: A. V. Promsky
Published: (2011-12-01) -
C-programs Verification on Basis of Mixed Axiomatic Semantics
by: I. S. Anureev, et al.
Published: (2010-09-01) -
Towards the ’Verified Verifier’. Theory and Practice
by: D. A. Kondratyev, et al.
Published: (2014-12-01)