Разработка самоприменимой системы верификации. Теория и практика


https://doi.org/10.18255/1818-1015-2014-6-71-82

Полный текст:


Аннотация

По сравнению с традиционным тестированием дедуктивная верификация предлагает более формальный способ доказательства корректности программ. Но как установить корректность самой системы верификации? Теоретические основы логик Хоара исследовались в классических работах, где были получены различные результаты по непротиворечивости и полноте. Однако нам не известны реализации этих теоретических методов, проверенные чем-либо отличным от обычного тестирования. Иными словами, нас интересует система верификации, которая может быть применена к самой себе (хотя бы частично). В наших исследованиях мы обратились к методу метагенерации, который выглядит многообещающим для этой задачи.


Об авторах

Дмитрий Александрович Кондратьев
Новосибирский государственный университет
Россия
студент, 630090, Россия, г. Новосибирск, ул. Пирогова, 2


Алексей Владимирович Промский
Институт систем информатики имени А.П. Ершова СО РАН
Россия
ст. науч. сотр., 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

Просмотров: 247

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)