Attribute Annotations and Their Use in C Program Deductive Verification

Autor:	M. M. Atuchin, I. S. Anureev
Jazyk:	English<br />Russian
Rok vydání:	2011
Předmět:	deductive verification attribute normalization attribute annotations axiomatic semantics c-light c-kernel Information technology T58.5-58.64
Zdroj:	Моделирование и анализ информационных систем, Vol 18, Iss 4, Pp 21-33 (2011)
Druh dokumentu:	article
ISSN:	1818-1015 2313-5417
Popis:	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.
Databáze:	Directory of Open Access Journals
Externí odkaz:	https://doaj.org/article/bf712c51f621466bbeecc7b3cd1c3389 Zobrazit plný text záznamu View record in DOAJ