Разработка самоприменимой системы верификации. Теория и практика
https://doi.org/10.18255/1818-1015-2014-6-71-82
Аннотация
По сравнению с традиционным тестированием дедуктивная верификация предлагает более формальный способ доказательства корректности программ. Но как установить корректность самой системы верификации? Теоретические основы логик Хоара исследовались в классических работах, где были получены различные результаты по непротиворечивости и полноте. Однако нам не известны реализации этих теоретических методов, проверенные чем-либо отличным от обычного тестирования. Иными словами, нас интересует система верификации, которая может быть применена к самой себе (хотя бы частично). В наших исследованиях мы обратились к методу метагенерации, который выглядит многообещающим для этой задачи.
Ключевые слова
верификация,
спецификация,
аксиоматическая семантика,
язык C-light,
условие корректности,
метагенерация
Об авторах
Дмитрий Александрович Кондратьев
Новосибирский государственный университет
Россия
студент, 630090, Россия, г. Новосибирск, ул. Пирогова, 2
Россия
студент, 630090, Россия, г. Новосибирск, ул. Пирогова, 2
Алексей Владимирович Промский
Институт систем информатики имени А.П. Ершова СО РАН
Россия
ст. науч. сотр., 630090, Россия, г. Новосибирск, пр. Лаврентьева, 6
Россия
ст. науч. сотр., 630090, Россия, г. Новосибирск, пр. Лаврентьева, 6
Список литературы
1. Apt K.R., Olderog E.R. Verification of sequential and concurrent programs. Berlin etc.: Springer, 1991. 450 p.
2. Cohen E., Dahlweid M., Hillebrand M.A., Leinenbach D., Moskal M., Santen T., Schulte W., Tobies S. VCC: A Practical System for Verifying Concurrent C // Proc. TPHOLs. 2009. LNCS. 2009. Vol. 5674. P. 23–42.
3. Filliˆatre J.C., March´e C. Multi-prover verification of C programs // Proc. ICFEM 2004. LNCS. 2004. Vol. 3308. P. 15–29.
4. Maryasov I.V., Nepomnyaschy V.A., Promsky A.V., Kondratyev D.A. Automatic C Program Verification Based on Mixed Axiomatic Semantics // Proc. Fourth Workshop "Program Semantics, Specification and Verification: Theory and Applications". Yekaterinburg, Russia, June 24, 2013. P. 50–59.
5. Moriconi M., Schwartz R.L. Automatic Construction of Verification Condition Generators From Hoare Logics // Lect. Notes Comput. Sci. Berlin etc., 1981. Vol. 115. P. 363–377.
6. Непомнящий В.А., Ануреев И.С., Михайлов И.Н., Промский А.В. Ориентированный на верификацию язык C-light // Системная информатика: Сб. науч. тр. Новосибирск: Издательство СО РАН, 2004. Вып. 9: Формальные методы и модели информатики. С. 51–134. [Nepomnyaschy V.A., Anureev I.S., Mikhaylov I.N., Promsky A.V. Orientirovannyy na verifikatsiyu yazyk C-light // Sistemnaya informatika: Sb. nauch. tr. Novosibirsk: Izdatel’stvo SO RAN, 2004. Vyp. 9: Formal’nye metody i modeli informatiki. S. 51–134 (in Russion)].
7. Norrish M. C formalised in HOL: Thes. doct. phylosophy (computer sci.). Cambridge, 1998. 150 p.
8. Oheimb D. von. Hoare logic for Java in Isabelle/HOL // Concurrency and Computation: Practice and Experience. 2001. 13(13).
9. Promsky A.V. C Program Verification: Verification Condition Explanation and Standard Library // Automatic Control and Computer Sciences. 2012. Vol. 46, No. 7. P. 394–401.
10. Promsky A.V. Experiments on self-applicability in the C-light verification system // Bull. Nov. Comp. Center, Comp. Science. 2013. 35. P. 85–99.
Рецензия
Для цитирования:
Кондратьев Д.А., Промский А.В. Разработка самоприменимой системы верификации. Теория и практика. Моделирование и анализ информационных систем. 2014;21(6):71-82. https://doi.org/10.18255/1818-1015-2014-6-71-82
For citation:
Kondratyev D.A., Promsky A.V. Towards the ’Verified Verifier’. Theory and Practice. Modeling and Analysis of Information Systems. 2014;21(6):71-82. (In Russ.) https://doi.org/10.18255/1818-1015-2014-6-71-82
Просмотров: 823
Послать статью по эл. почте 