Пример верификации в проекте F@BOOL@, основанном на булевских решателях

Н. В. Шилов

doi:undefined

Пример верификации в проекте F@BOOL@, основанном на булевских решателях

Н. В. Шилов

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

Аннотация

Верифицирующий компилятор - это системная компьютерная программа, которая транслирует написанные человеком программы с языка высокого уровня в эквивалентные исполнимые программы и, кроме того, доказывает (верифицирует) специфицированные человеком математические утверждения о свойствах транслируемых программ. Цель проекта F@BOOL@ - разработка понятного для пользователей, компактного и переносимого верифицирующего компилятора аннотированных вычислительных программ, использующего эффективные и достоверные автоматические SAT-решатели в качестве средств автоматической проверки истинности условий корректности (вместо средств полуавтоматического доказательства). В период с 2006 по 2009 гг. в проекте F@BOOL@ использовался SAT-решатель zChaff. С его помощью были выполнены первые эксперименты по верификации простых программ на Mini-NIL: программы обмена переменных своими значениями, проверки троек целых чисел быть длинами сторон равностороннего или равнобедренного треугольника, и поиска одной фальшивой среди 15 монет с использованием чашечных весов. В работе рассказано об основных идеях проекта F@BOOL@ и приведены детали эксперимента по верификации программы, решающей головоломку о монетах.

Ключ. слова

формальная верификация программ, операционная и трансформационная семантика программ, метод верификации Флойда - Хоара, условия корректности, булевские решатели,

УДК: 519.681+519.682.1

Об авторе

Н. В. Шилов

Институт систем информатики им. А.П. Ершова СО РАН, Новосибирский государственный университет и Новосибирский государственный технический университет
Россия

Список литературы

1. Ахо А., Хопкрофт Дж., Ульман Дж. Построение и анализ вычислительных алгоритмов. М.: Мир. 1979.

2. Бодин Е.В., Калинина Н.А., Шилов Н.В. Проект верифицирующего компилятора F@BOOL@ Часть I: Общее описание проекта F@BOOL@, его место в компонентном подходе к программированию. Язык Mini-NIL - прототип языка виртуальной машины проекта. Препринт №131 Института систем информатики им. А.П. Ершова СО РАН, 2005.

3. Бодин Е.В., Калинина Н.А., Шилов Н.В. Проект верифицирующего компилятора F@BOOL@. Часть II: Логические аннотации в языке Mini-NIL, их статическая семантика и семантика времени исполнения. Препринт №138 Института систем информатики им. А.П. Ершова СО РАН, 2006.

4. Дейкстра В.Э. Дисциплина программирования. М.: Мир, 1978.

5. Грис Д. Наука программирования. М.: Мир, 1984.

6. Шилов Н.В., Бодин Е.В. Ии И. О программных логиках - просто // Системная информатика, выпуск 8. Новосибирск: Наука, 2002. С. 206-249.

7. Шилов Н.В., Ануреев И.С., Бодин Е.В. О генерации условий корректности для императивных программ // Программирование. 2008, №6. С. 1-20.

8. Шилов Н.В. Заметки о трёх парадигмах программирования // Компьютерные инструменты в образовании. 2010, №2. С. 24-37.

9. Anureev I.S., Bodin E.V., Gorodnyaya L.V., Marchuk A.G., Murzin F.A., Shilov N.V. On the Problem of Computer Language Classification // Joint NCC&IIS Bulletin, Series Computer Science. 2008. Vol. 28. P. 1-29.

10. Ball T., Cook B., Levin V., and Rajamani S. K. SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft // Springer-Verlag, Berlin, LNCS. 2004. Vol. 2999. P. 1-20.

11. Beyer D., Henzinger T.A., Jhala R., and Majumdar R. The Software Model Checker Blast: Applications to Software Engineering // Int. Journal on Software Tools for Technology Transfer. 2007. N 9. P. 505-525.

12. Floyd R.W. Assigning meanings to programs. Proc. of a Symposium in Applied Mathematics. Mathematical Aspects of Computer Science, Vol. 19. American Math. Society, Providence, R. I., 1967. P. 19-32.

13. Hoare C. A. R. The Verifying Compiler: A Grand Challenge for Computing Research. Perspectives of Systems Informatics (PSI'2003), Springer-Verlag, Berlin, LNCS. Vol. 2890. 2003. P. 1-12.

14. Shilov N.V., Bodin Eu.V, Shilova S.O. Fabulous arrays I: Operational and transformational semantics of static arrays in vericationproject F@BOOL@. Bull. Nov. Comp. Center, Comp. Science. Vol. 29. 2009. P. 121-140.

Дополнительные файлы

Для цитирования: Шилов Н.В. Пример верификации в проекте F@BOOL@, основанном на булевских решателях. Моделирование и анализ информационных систем. 2010;17(4):111-124.

For citation: Shilov N.V. F@BOOL@: experiment with a simple verifying compiler based on SAT-solvers. Modeling and Analysis of Information Systems. 2010;17(4):111-124. (In Russ.)

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

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

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

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

Логин
Пароль