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...

Full description

Bibliographic Details
Main Authors: M. M. Atuchin, I. S. Anureev
Format: Article
Language:English
Published: Yaroslavl State University 2011-12-01
Series:Modelirovanie i Analiz Informacionnyh Sistem
Subjects:
Online Access:https://www.mais-journal.ru/jour/article/view/1095