Attribute Annotations and Their Use in C Program Deductive Verification
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
MSC2020: 519.681
About the Authors
M. M. Atuchin
Институт систем информатики имени А.П. Ершова СО РАН
Russian Federation
Russian Federation
I. S. Anureev
Институт систем информатики имени А.П. Ершова СО РАН
Russian Federation
Russian Federation
References
1. Leroy X. Formal verification of a realistic compiler // Communications of the ACM. 2009. 52(7). P. 107-115.
2. Filliatre J. C., Marche C. Multi-prover verification of C programs // Proc. ICFEM 2004. 2004. LNCS 3308. P. 15-29.
3. Leino K.R.M., Rummer P. A polymorphic intermediate verification language: Design and logical encoding // TACAS 2010. 2010. LNCS 6015. P. 312-327.
4. Leino K. R. M. Dafny: an automatic program verifier for functional correctness // LPAR-16. 2010. LNCS 6355. P. 348-370.
5. Cohen E., Dahlweid M, Hillebrand M., et al. VCC: A Practical System for Veirying Concurrent C // TPHOLs 2009. 2009. LNCS 5674. P. 23-42.
6. Alkassar E., Hillebrand M.A., Leinenbach D., Schirmer N.W., Starostin A. The Verisoft Approach to Systems Verification // VSTTE 2008. 2008. LNCS 5295. P. 209224.
7. Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. № 6. С. 5-15.
8. Nepomniaschy, V. A., Anureev, I. S., Promsky, A. V. Verification-oriented language C- light and its structural operational semantics // Proc. of Conf. PSI-2003. 2003. LNCS 2890. P. 1-5.
9. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика // Программирование. 2002. № 6. С. 1-13.
10. Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации C- программ. Язык С-light и его трансформационная семантика // Проблемы программирования. 2006. № 2-3. С. 359-368.
11. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Формальные методы и модели информатики: Сборник научных трудов. Серия "Системная информатика". Новосибирск: Издательство СО РАН. 2004. № 9. C. 51-134.
12. Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C-программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Том 17, № 3. С. 5-28.
13. ISO/IEC 9899: Programming languages - C. (1999)
14. Nepomniaschy V.A., Sulimov A.A. Promlem-oriented means of program specification and verification in project SPECTRUM // DISCo 1993. 1993. LNCS 722. P. 374-378.
15. Nepomniaschy V.A., Sulimov A.A. Problem-oriented verification system and its application to linear algebra programs // Theoretical Computer Science. 1993. 119. P. 173-185.
16. Непомнящий В.А., Ануреев И.С., Промский А.В., Дубрановский И.В. На пути к верификации C# программ: трехуровневый подход // Программирование. 2006. № 4. С. 4-20.
17. Anureev I.S. Introduction to the Atoment language // Joint NCC&IIS Bulletin, Series Computer Science. 2010. Vol. 30. P. 1-16.
18. Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В. Система анализа и верификации C-программ СПЕКТР-2 // Моделирование и анализ информационных систем. 2010. Том 17, № 4. С. 88-100.
Review
For citations:
Atuchin M.M., Anureev I.S. Attribute Annotations and Their Use in C Program Deductive Verification. Modeling and Analysis of Information Systems. 2011;18(4):21-33. (In Russ.)
Views:
573
Email this article 