|
Modelirovanie i Analiz Informatsionnykh Sistem, 2011, Volume 18, Number 4, Pages 21–33
(Mi mais195)
|
|
|
|
This article is cited in 2 scientific papers (total in 2 papers)
Attribute annotations and their use in C program deductive verification
M. M. Atuchin, I. S. Anureev A. P. Ershov Institute of Informatics Systems Sib. Br. RAS
Abstract:
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.
Keywords:
deductive verification, attribute normalization, attribute annotations, axiomatic semantics, C-light, C-kernel.
Received: 09.10.2011
Citation:
M. M. Atuchin, I. S. Anureev, “Attribute annotations and their use in C program deductive verification”, Model. Anal. Inform. Sist., 18:4 (2011), 21–33
Linking options:
https://www.mathnet.ru/eng/mais195 https://www.mathnet.ru/eng/mais/v18/i4/p21
|
Statistics & downloads: |
Abstract page: | 270 | Full-text PDF : | 90 | References: | 37 |
|