Атрибутные аннотации и их применение в дедуктивной верификации C-программ
Аннотация
Предложен новый вид аннотаций, называемых атрибутными аннотациями, и методология их применения в дедуктивной верификации программ. Описана коллекция аннотирующих атрибутов для подмножества C-kernel языка C и на их основе представлены два варианта аксиоматической семантики языка C- kernel - семантика прямого прослеживания и смешанная семантика прямого прослеживания.
Ключевые слова
дедуктивная верификация,
атрибутная нормализация,
атрибутные аннотации,
аксиоматическая семантика,
C-light,
C-kernel
MSC2020: 519.681
Об авторах
Михаил Михайлович Атучин
Институт систем информатики имени А.П. Ершова СО РАН
Россия
Россия
Игорь Сергеевич Ануреев
Институт систем информатики имени А.П. Ершова СО РАН
Россия
Россия
Список литературы
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.
Рецензия
Для цитирования:
Атучин М.М., Ануреев И.С. Атрибутные аннотации и их применение в дедуктивной верификации C-программ. Моделирование и анализ информационных систем. 2011;18(4):21-33.
For citation:
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.)
Просмотров:
566
Послать статью по эл. почте 