References

mais

Моделирование и анализ информационных систем

Modeling and Analysis of Information Systems

1818-10152313-5417

Yaroslavl State University

mais-1095

Research Article

Оригинальные статьи

Articles

Атрибутные аннотации и их применение в дедуктивной верификации C-программ

Attribute Annotations and Their Use in C Program Deductive Verification

Атучин

Михаил Михайлович

Atuchin

M. M.

atuchinm@gmail.com

Ануреев

Игорь Сергеевич

Anureev

I. S.

anureev@iis.nsk.su

Институт систем информатики имени А.П. Ершова СО РАНRussian Federation

2011

20122011

1842133

2011

Атучин М.М., Ануреев И.С.

Atuchin M.M., Anureev I.S.

Данная работа распространяется под лицензией Creative Commons Attribution 4.0.

This work is licensed under a Creative Commons Attribution 4.0 License.

https://www.mais-journal.ru/jour/article/view/1095

Предложен новый вид аннотаций, называемых атрибутными аннотациями, и методология их применения в дедуктивной верификации программ. Описана коллекция аннотирующих атрибутов для подмножества C-kernel языка C и на их основе представлены два варианта аксиоматической семантики языка C- kernel - семантика прямого прослеживания и смешанная семантика прямого прослеживания.

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.

дедуктивная верификацияатрибутная нормализацияатрибутные аннотацииаксиоматическая семантикаC-lightC-kernel

deductive verificationattribute normalizationattribute annotationsaxiomatic semanticsC-lightC-kernel

References1

Leroy X. Formal verification of a realistic compiler // Communications of the ACM. 2009. 52(7). P. 107-115.

Filliatre J. C., Marche C. Multi-prover verification of C programs // Proc. ICFEM 2004. 2004. LNCS 3308. P. 15-29.

Leino K.R.M., Rummer P. A polymorphic intermediate verification language: Design and logical encoding // TACAS 2010. 2010. LNCS 6015. P. 312-327.

Leino K. R. M. Dafny: an automatic program verifier for functional correctness // LPAR-16. 2010. LNCS 6355. P. 348-370.

Cohen E., Dahlweid M, Hillebrand M., et al. VCC: A Practical System for Veirying Concurrent C // TPHOLs 2009. 2009. LNCS 5674. P. 23-42.

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.

Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации С программ. Аксиоматическая семантика языка C-kernel // Программирование. 2003. № 6. С. 5-15.

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.

Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. На пути к верификации С программ. Язык C-light и его формальная семантика // Программирование. 2002. № 6. С. 1-13.

Непомнящий В.А., Ануреев И.С., Промский А.В. На пути к верификации C- программ. Язык С-light и его трансформационная семантика // Проблемы программирования. 2006. № 2-3. С. 359-368.

Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Формальные методы и модели информатики: Сборник научных трудов. Серия "Системная информатика". Новосибирск: Издательство СО РАН. 2004. № 9. C. 51-134.

Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C-программ на основе смешанной аксиоматической семантики // Моделирование и анализ информационных систем. 2010. Том 17, № 3. С. 5-28.

ISO/IEC 9899: Programming languages - C. (1999)

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.

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.

Непомнящий В.А., Ануреев И.С., Промский А.В., Дубрановский И.В. На пути к верификации C# программ: трехуровневый подход // Программирование. 2006. № 4. С. 4-20.

Anureev I.S. Introduction to the Atoment language // Joint NCC&IIS Bulletin, Series Computer Science. 2010. Vol. 30. P. 1-16.

Непомнящий В.А., Ануреев И.С., Атучин М.М., Марьясов И.В., Петров А.А., Промский А.В. Система анализа и верификации C-программ СПЕКТР-2 // Моделирование и анализ информационных систем. 2010. Том 17, № 4. С. 88-100.

The authors declare that there are no conflicts of interest present.