Верификация C-программ на основе смешанной аксиоматической семантики
Аннотация
Ключевые слова
MSC2020: 519.681.3
Об авторах
И. С. АнуреевРоссия
И. В. Марьясов
Россия
В. А. Непомнящий
Россия
Список литературы
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.
Рецензия
Для цитирования:
Ануреев И.С., Марьясов И.В., Непомнящий В.А. Верификация C-программ на основе смешанной аксиоматической семантики. Моделирование и анализ информационных систем. 2010;17(3):5-28.
For citation:
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.)