DOI: 10.17587/prin.7.202-210

УДК: 519.683.2

Система дедуктивной верификации предикатных программ

М. С. Чушкин, аспирант, e-mail: chushkinm@rambler.ru, Институт систем информатики им. А. П. Ершова, г. Новосибирск

Представлен новый метод генерации формул тотальной корректности рекурсивных программ без циклов и указателей. Реализована система дедуктивной верификации, генерирующая формулы корректности. Разработана система правил для упрощения процесса генерации формул корректности. Истинность полученных формул проверена с помощью SMT-решателя CVC3 и в системе PVS.

Ключевые слова: предикатное программирование, тотальная корректность программы, дедуктивная верификация, система автоматического доказательства PVS, SMT-решатель CVC3

Стр. 202–210

Работа выполнена при поддержке РФФИ, грант № 16-01-00498