C-programs Verification on Basis of Mixed Axiomatic Semantics
Abstract
The mixed axiomatic semantics of a C-kernel language is described. This language is the kernel of a representative C language subset which is callexl C-light. Such semantics allows to simplify the verification conditions in many cases. This semantics is a base of verification conditions generator of C-kernel programs. An example which illustrates the use of inference rules of the semantics is considered.
Keywords
program verification,
operational semantics,
axiomatic semantics,
C language,
C-light language,
C-kernel language,
partial correxctness
MSC2020: 519.681.3
About the Authors
I. S. Anureev
Институт систем информатики им. А. П. Ершова СО РАН
Russian Federation
Russian Federation
I. V. Maryasov
Институт систем информатики им. А. П. Ершова СО РАН
Russian Federation
Russian Federation
V. A. Nepomniaschy
Институт систем информатики им. А. П. Ершова СО РАН
Russian Federation
Russian Federation
References
1. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. Ориенти¬рованный на верификацию язык C-light // Системная информатика: сборник научных трудов. Новосибирск: Издательство СО РАН. 2004. Вып. 9: Формаль¬ные методы и модели информатики. С. 51 - 134.
2. Непомнящий В. А., Ануреев И. С., Промский А. В. На пути к верификации C-программ. Язык C-light и его трансформационная семантика // Problems in Programming. Kiev, 2006. № 2 - 3. С. 359 - 368.
3. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пу¬ти к верификации C программ. Язык C-light и его формальная семантика // Программирование. 2002. № 6. С. 19 - 30.
4. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации C программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. № 6. С. 5 - 15.
5. Непомнящий В. А., Ануреев И. С., Михайлов И. Н., Промский А. В. На пути к верификации С программ. Часть 1. Язык C-light. Новосибирск, 2001. 48 с. (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 84).
6. Марьясов И. В. На пути к автоматической верификации C-light программ. Сме¬шанная аксиоматическая семантика языка C-kernel. Новосибирск, 2008. 32 с. (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 150).
7. Марьясов И. В. Применение смешанной аксиоматической семантики языка C-kernel к верификации программы топологической сортировки. - Новосибирск, 2010. - 33 с. - (Препр. / РАН. Сиб. Отд-ние. ИСИ; № 155).
8. Непомнящий В. А., Рякин, О. М. Прикладные методы верификации программ. М.: Радио и связь, 1988.
9. Programming languages - C: ISO/IEC 9899:1999. 1999. 566 p.
10. Maryasov I. V. Towards automatic verification of C-light programs. Mixed axiomatic semantics of C-kernel language // Perspectives of Systems Informatics (PSI): A. Ershov 7th Int. Conf.: Int. workshop on Program Understanding. Novosibirsk, 2009. P. 44 - 52.
11. Norrish M. C formalised in HOL: Thes. doct. phylosophy (computer sci.). Cambridge, 1998. 150 p.
Review
For citations:
Anureev I.S., Maryasov I.V., Nepomniaschy V.A. C-programs Verification on Basis of Mixed Axiomatic Semantics. Modeling and Analysis of Information Systems. 2010;17(3):5-28. (In Russ.)
Views:
556
Email this article 