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...
| Main Authors: | , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Yaroslavl State University
2011-12-01
|
| Series: | Моделирование и анализ информационных систем |
| Subjects: | |
| Online Access: | https://www.mais-journal.ru/jour/article/view/1095 |
| _version_ | 1797877970909528064 |
|---|---|
| author | M. M. Atuchin I. S. Anureev |
| author_facet | M. M. Atuchin I. S. Anureev |
| author_sort | M. M. Atuchin |
| collection | DOAJ |
| description | 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 semantics of C-kernel - forward semantics and mixed forward semantics - are presented. |
| first_indexed | 2024-04-10T02:25:18Z |
| format | Article |
| id | doaj.art-bf712c51f621466bbeecc7b3cd1c3389 |
| institution | Directory Open Access Journal |
| issn | 1818-1015 2313-5417 |
| language | English |
| last_indexed | 2024-04-10T02:25:18Z |
| publishDate | 2011-12-01 |
| publisher | Yaroslavl State University |
| record_format | Article |
| series | Моделирование и анализ информационных систем |
| spelling | doaj.art-bf712c51f621466bbeecc7b3cd1c33892023-03-13T08:07:31ZengYaroslavl State UniversityМоделирование и анализ информационных систем1818-10152313-54172011-12-011842133836Attribute Annotations and Their Use in C Program Deductive VerificationM. M. Atuchin0I. S. Anureev1Институт систем информатики имени А.П. Ершова СО РАНИнститут систем информатики имени А.П. Ершова СО РАН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 semantics of C-kernel - forward semantics and mixed forward semantics - are presented.https://www.mais-journal.ru/jour/article/view/1095дедуктивная верификацияатрибутная нормализацияатрибутные аннотацииаксиоматическая семантикаc-lightc-kernel |
| spellingShingle | M. M. Atuchin I. S. Anureev Attribute Annotations and Their Use in C Program Deductive Verification Моделирование и анализ информационных систем дедуктивная верификация атрибутная нормализация атрибутные аннотации аксиоматическая семантика c-light c-kernel |
| title | Attribute Annotations and Their Use in C Program Deductive Verification |
| title_full | Attribute Annotations and Their Use in C Program Deductive Verification |
| title_fullStr | Attribute Annotations and Their Use in C Program Deductive Verification |
| title_full_unstemmed | Attribute Annotations and Their Use in C Program Deductive Verification |
| title_short | Attribute Annotations and Their Use in C Program Deductive Verification |
| title_sort | attribute annotations and their use in c program deductive verification |
| topic | дедуктивная верификация атрибутная нормализация атрибутные аннотации аксиоматическая семантика c-light c-kernel |
| url | https://www.mais-journal.ru/jour/article/view/1095 |
| work_keys_str_mv | AT mmatuchin attributeannotationsandtheiruseincprogramdeductiveverification AT isanureev attributeannotationsandtheiruseincprogramdeductiveverification |