Разработка автоматизированного средства для доказательства свойств программ | Прикладная дискретная математика. 2014. № 7 (Приложение).

Рассматривается метод статической верификации программ, основанный на автоматизированном доказательстве теорем. Моделью программы выбраны функции на парах списков натуральных чисел, упрощённой моделью - функции на натуральных числах. Исследуется свойство безопасности: программа может выдать секретное сведение, только если на вход был подан ключ. С помощью автоматизированного средства доказательства теорем Coq строятся доказательства для примеров функций, выводится общая схема построения доказательств, с помощью которой создаётся тактика Coq. В заключение приводятся идеи дальнейших исследований.