Введение 4
1. Постановка задачи 7
2. Обзор 8
2.1. Основные определения
2.2. Проект Z3
2.3. Проект SPACER .
2.4. Проект VeriMAPRel
3. Алгоритм синхронного произведения ограниченных дизъюнктов
Хорна 12
4. Алгоритм поиска синхронизационных лемм 16
4.1. Граф достижимости правил
4.2. Первый подход
4.3. Второй подход
5. Реализация и эксперименты 26
Заключение 28
Список литературы
Компьютеры стали незаменимой частью современного мира и контролируют все большее количество его аспектов. С учетом этого вопросы корректности программ выходят на первый план. Наряду с традиционной ручной разработкой тестов существуют подходы по автоматической генерации тестового покрытия, формальной верификации и синтеза программного кода.
С середины 2000-х годов в контексте всех трех направлений особую популярность приобрели системы автоматического доказательства теорем для задачи SMT1 — SMT-решатели [4, 7, 8, 19]. Задача SMT заключается в том, чтобы определить выполнима ли формула языка первого порядка, где функции и предикатные символы интерпретированы согласно заранее заданным теориям. Другими словами, задача SMT аналогична задаче выполнимости булевых формул (задаче SAT), но булевы переменные обобщены до предикатов заранее заданных теорий, а также возможно появление кванторов. Например, линейные неравенства над вещественными или целочисленными переменными (2x + 4y ≥ 6) являются предикатами множества теории линейной вещественной или целочисленной арифметики и вычисляются согласно правилам этих теорий. Помимо теорий линейной целочисленной и вещественной арифметики, SMT-решатели могут поддерживать теории массивов и алгебраических типов данных, теории битовых векторов, строк, неинтерпретируемых функций. SMT-решатели эффективно комбинируют алгоритмы решения задачи SAT (как, к примеру, DPLL [6]) с разрешающими процедурами теорий.
Несмотря на все преимущества, SMT-решатели плохо подходят для рассуждения о рекурсивных программах. Доказательство безопасности программы, как правило, опирается на поиск безопасного индуктивного инварианта. Для программы < Init; Tr; P >, где Init — начальное состояние, Tr — отношение перехода программы, а P — свойство безопасности программы, безопасный индуктивный инвариант Inv должен Satisfiability Modulo Theories — задача выполнимости формул в теориях удовлетворять следующим 3 свойствам:
8u 2 S (Init(u) ) Inv(u))
8u; v 2 S (Inv(u) ^ T r(u; v) ) Inv(v))
8u 2 S (Inv(u) ) P(u));
где S — множество состояний программы.
Проблема заключается в том, что задача поиска безопасного индуктивного инварианта для рекурсивных программ не выражается в логике первого порядка.
Тем не менее в последние пять лет активно развивается подход, вдохновленный логическим программированием [12], в котором программа описывается в виде набора ограниченных дизъюнктов Хорна
— формул логики первого порядка особого вида, где помимо интерпретированных функциональных и предикатных символов имеется множество неинтерпретированных реляционных символов (формальное определение дано в главе 2). Инструменты, решающие такие системы (далее — Хорн-решатели), используют всю инфраструктуру SMT-решателей и современные подходы, использующиеся для верификации программного кода [5, 10, 11, 14, 21]. В случае, когда Хорн-решатель завершается на системе ограниченных дизъюнктов Хорна, результатом его работы будет служить либо доказательство выполнимости системы дизъюнктов Хорна (индуктивный инвариант безопасности), либо контрпример в виде дерева вывода.
Возможна, однако, ситуация, когда индуктивный инвариант безопасности системы не выражается в теориях Хорн-решателей, и процесс
поиска решения не завершается. Ценными в таком случае являются методы ослабления индуктивного инварианта. Недавно в статье [15] была предложена операция синхронного произведения ограниченных дизъюнктов Хорна, которая во многих случаях трансформирует систему ограниченных дизъюнктов Хорна таким образом, что не решающиеся современными Хорн-решателями системы начинают решаться за доли секунды.
Алгоритм, представленный в упомянутой статье [15], был реализован и протестирован на базе системы Rosette [22]. Система Rosette не так популярна, как Хорн-решатели Z3 [7] или SPACER [1, 14], и, т.к.
она является «надстройкой» над ними, реализация алгоритма синхронизации на уровне Rosette не позволяет получить всех преимуществ от тесной интеграции с ядром Z3, как в случае расширения кодовой базы непосредственно Z3.
Поздние эксперименты показали, что возможно улучшить алгоритм синхронного произведения с помощью вычисления синхронизационных лемм — индуктивных утверждений, описывающих связь двух или более
цепочек рекуррентных вычислений. Задача синхронизационных лемм состоит в определении
необходимости проведения операции синхронного произведения, а также в облегчении поиска безопасного индуктивного инварианта.
В рамках данной работы было сделано следующее.
1. Изучен и реализован алгоритм синхронизации дизъюнктов Хорна для Хорн-решателей Z3 и SPACER.
2. Реализован алгоритм поиска синхронизационных лемм, основанный на отбрасывании конъюнктов.
3. Реализован алгоритм поиска синхронизационных лемм, основанный на формировании нового запроса к Хорн-решателю.
4. Поставлены эксперименты с решателем SPACER без синхронизации и с алгоритмом синхронного произведения, улучшенного с помощью синхронизационных лемм.
