Разработка автоматизированного средства для доказательства свойств программ

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