Выполнимость по модулю теорий

В информатике и математической логике выполнимость по модулю теорий (SMT ) - это проблема решения для логических формул относительно комбинаций фоновых теорий, выраженных в классической логике первого порядка с равенством. Примерами теорий, обычно используемых в информатике, являются теория действительных чисел, теория целых чисел и теории различных структур данных, таких как перечисляет, массивы, битовые векторы и так далее. SMT можно рассматривать как форму проблемы удовлетворения ограничений и, таким образом, определенный формализованный подход к программированию ограничений.

• 1 Базовая терминология
• 2 Выразительная сила
• 3 Решающие подходы
• 4 SMT для неразрешимых теорий
• 5 Решатели
  • 5.1 Стандартизация и соревнование решателей SMT-COMP
• 6 Приложения
  • 6.1 Проверка
  • 6.2 Анализ и тестирование на основе символьного исполнения
• 7 См. Также
• 8 Примечания
• 9 Ссылки

Формально говоря, экземпляр SMT - это формула в логике первого порядка, где некоторые функции и предикатные символы имеют дополнительные интерпретации, а SMT - это проблема определения выполнимости такой формулы. Другими словами, представьте себе пример проблемы логической выполнимости (SAT), в которой некоторые из двоичных переменных заменены предикатами над подходящим набором недвоичных переменных. Предикат - это двоичная функция недвоичных переменных. Примеры предикатов включают линейные неравенства (например, $3\; x\; +\; 2\; y\; -\; z\; \ge \; 4\; \{\backslash \; displaystyle\; 3x\; +\; 2y-z\; \backslash \; geq\; 4\}$) или равенства, содержащие неинтерпретированные термины и функциональные символы (например, $f\; (f\; (u,\; v),\; v)\; =\; f\; (u,\; v)\; \{\backslash \; displaystyle\; f\; (f\; (u,\; v),\; v)\; =\; f\; (\; u,\; v)\}$, где $f\; \{\backslash \; displaystyle\; f\}$- некоторая неопределенная функция двух аргументов). Эти предикаты классифицируются согласно каждой присвоенной теории. Например, линейные неравенства над действительными переменными оцениваются с использованием правил теории линейной вещественной арифметики, тогда как предикаты, содержащие неинтерпретированные термины и функциональные символы, оцениваются с использованием правил теории неинтерпретированных функций с равенством (иногда называемое пустой теорией ). Другие теории включают теории массивов и списков структур (полезно для моделирования и проверки компьютерных программ ) и теорию битовых векторов (полезно при моделировании и проверке проектов оборудования ). Также возможны подтеории: например, разностная логика - это подтеория линейной арифметики, в которой каждое неравенство ограничено формой $x\; -\; y>c\; \{\backslash \; displaystyle\; xy>c\}$для переменных <151style>x { x}и $y\; \{\backslash \; displaystyle\; y\}$и константа $c\; \{\backslash \; displaystyle\; c\}$.

Большинство решателей SMT поддерживают только квантификатор -свободные фрагменты их логики.

Экземпляр SMT является обобщением логического экземпляра SAT, в котором различные наборы переменных заменяются на предикаты из множества лежащих в основе теорий. Формулы SMT предоставляют гораздо более богатый язык моделирования, чем это возможно с логическими формулами SAT. Например, формула SMT позволяет нам моделировать путь данных операций микропроцессора на rd, а не битовый уровень.

Для сравнения, программирование набора ответов также основано на предикатах (точнее, на атомарных предложениях, созданных из атомарной формулы ). В отличие от SMT, программы с набором ответов не имеют кванторов и не могут легко выразить ограничения, такие как или —ASP в лучшем случае подходит для логических задач, которые сводятся к свободной теории неинтерпретированных функций. Реализация 32-битных целых чисел в качестве битовых векторов в ASP страдает от большинства проблем, с которыми сталкивались ранние SMT-решатели: «очевидные» идентичности, такие как x + y = y + x, трудно вывести.

Программирование логики ограничений действительно обеспечивает поддержку линейных арифметических ограничений, но в совершенно другой теоретической структуре. Решатели SMT также были расширены для решения формул в логике более высокого порядка.

Ранние попытки решения экземпляров SMT включали преобразование их в логические экземпляры SAT (например, 32-битную целочисленную переменную будут закодированы 32 однобитными переменными с соответствующими весами, а операции на уровне слова, такие как «плюс», будут заменены логическими операциями более низкого уровня над битами) и передать эту формулу в логический решатель SAT. Этот подход, который называется подходом нетерпеливым, имеет свои достоинства: путем предварительной обработки формулы SMT в эквивалентную булеву формулу SAT существующие булевы решатели SAT могут использоваться «как есть» и их производительность и улучшения емкости со временем. С другой стороны, потеря высокоуровневой семантики лежащих в основе теорий означает, что логическая программа расчета SAT должна работать намного усерднее, чем необходимо, чтобы обнаружить «очевидные» факты (например, $x\; +\; y\; =\; y\; +\; x\; \{\backslash \; displaystyle\; x\; +\; y\; =\; y\; +\; x\}$для сложения целых чисел.) Это наблюдение привело к разработке ряда решателей SMT, которые тесно интегрируют логические рассуждения DPLL - поиск стиля с помощью специальных решателей (T-решателей), которые обрабатывают конъюнкции (AND) предикатов из данной теории. Этот подход называется ленивым подходом.

Названная DPLL (T), эта архитектура возлагает ответственность за логические рассуждения на основанный на DPLL решатель SAT, который, в свою очередь, взаимодействует с решателем теории T через четко определенный интерфейс. Решателю теории нужно беспокоиться только о проверке выполнимости конъюнкций предикатов теории, переданных ему из решателя SAT, когда он исследует логическое пространство поиска формулы. Однако для того, чтобы эта интеграция работала хорошо, решатель теории должен иметь возможность участвовать в распространении и анализе конфликтов, т. Е. Он должен уметь выводить новые факты из уже установленных фактов, а также давать краткие объяснения неосуществимости, когда теория противоречит возникают. Другими словами, теоретический решатель должен быть инкрементным и с возможностью возврата.

Большинство распространенных подходов SMT поддерживают разрешимые теории. Однако многие реальные системы можно смоделировать только с помощью нелинейной арифметики над действительными числами, включая трансцендентные функции, например самолет и его поведение. Этот факт побуждает распространить проблему SMT на нелинейные теории, например определить, является ли

где

$b\; \in \; B,\; x,\; y\; \in \; R\; \{\backslash \; displaystyle\; b\; \backslash \; in\; \{\backslash \; mathbb\; \{B\}\},\; x,\; y\; \backslash \; in\; \{\backslash \; mathbb\; \{R\}\}\}$

выполнимо. Тогда такие проблемы становятся неразрешимыми в целом. (Теория реальных замкнутых полей и, таким образом, полная теория первого порядка действительных чисел, однако разрешима с использованием исключения кванторов. Это связано с Альфредом Тарским.) Теория первого порядка натуральных чисел со сложением (но не умножением), называемая арифметика Пресбургера, также разрешима.. Грех Поскольку умножение на константы может быть реализовано как вложенное сложение, арифметика во многих компьютерных программах может быть выражена с помощью арифметики Пресбургера, что приводит к разрешимым формулам.

Примерами SMT-решателей, обращающимися к булевым комбинациям теоретических атомов из неразрешимых арифметических теорий над действительными числами, являются ABsolver, в котором используется классическая архитектура DPLL (T) с пакетом нелинейной оптимизации в качестве (обязательно неполного) решателя подчиненной теории, и iSAT [1], основанный на объединении DPLL-решения SAT и распространения ограничений интервала, называемого алгоритмом iSAT.

В приведенной ниже таблице приведены некоторые функции многих доступных решателей SMT. Столбец «SMT-LIB» указывает совместимость с языком SMT-LIB; многие системы, отмеченные «да», могут поддерживать только старые версии SMT-LIB или предлагать только частичную поддержку языка. Столбец «CVC» указывает на поддержку языка CVC. Столбец «DIMACS» указывает на поддержку формата DIMACS.

Проекты различаются не только функциями и производительностью, но и жизнеспособностью окружающего сообщества, его постоянным интересом к проекту и его способностью вносить документацию, исправления, тесты и улучшения.

Стандартизация и конкуренция между решателями SMT-COMP

Есть несколько mpts для описания стандартизованного интерфейса для решателей SMT (и автоматических средств доказательства теорем, термин, часто используемый как синоним). Самым известным является стандарт SMT-LIB, который предоставляет язык, основанный на S-выражениях. Другие широко поддерживаемые стандартизованные форматы - это формат DIMACS, поддерживаемый многими логическими программами SAT-решения, и формат CVC, используемый автоматическим средством доказательства теорем CVC.

Формат SMT-LIB также поставляется с рядом стандартизированных тестов и позволяет проводить ежегодное соревнование между решателями SMT под названием SMT-COMP. Первоначально конкурс проводился во время конференции Computer Aided Verification (CAV), но с 2020 года конкурс проводится в рамках семинара SMT, который связан с Международной совместной конференцией по Automated Reasoning (IJCAR).

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

Верификация

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

Существует множество верификаторов, построенных на основе решателя SMT Z3. Boogie - это язык промежуточной проверки, использующий Z3 для автоматической проверки простых императивных программ. Верификатор VCC для параллельного C использует Boogie, а также Dafny для императивных объектно-ориентированных программ, Chalice для параллельных программ и Spec # для C #. F * - язык с зависимой типизацией, использующий Z3 для поиска доказательств; компилятор передает эти доказательства для создания байт-кода, несущего доказательство. Инфраструктура проверки Viper кодирует условия проверки в Z3. Библиотека sbv обеспечивает проверку программ Haskell на основе SMT и позволяет пользователю выбирать среди ряда решателей, таких как Z3, ABC, Boolector, CVC4, MathSAT и Yices.

Существует также множество верификаторов, построенных на основе решателя Alt-Ergo SMT. Вот список зрелых приложений:

• Why3, платформа для дедуктивной проверки программ, использует Alt-Ergo в качестве основного средства проверки;
• CAVEAT, средство проверки C, разработанное CEA и используемое Airbus; Alt-Ergo был включен в квалификацию DO-178C одного из своих последних самолетов;
• Frama-C, фреймворк для анализа C-кода, использует Alt-Ergo в плагинах Jessie и WP (посвященных " дедуктивная проверка программы ");
• SPARK, использует CVC4 и Alt-Ergo (за GNATprove) для автоматизации проверки некоторых утверждений в SPARK 2014;
• Atelier-B может вместо этого использовать Alt-Ergo своего основного доказателя (увеличение успеха с 84% до 98% в тестах ANR Bware project );
• Rodin, фреймворк B-метода, разработанный Systerel, может использовать Alt-Ergo в качестве серверной части;
• Cubicle, средство проверки моделей с открытым исходным кодом для проверки свойств безопасности систем перехода на основе массивов.
• EasyCrypt, набор инструментов для анализа реляционных свойств вероятностных вычислений с противостоящим кодом.

Многие Решатели SMT реализуют общий формат интерфейса под названием SMTLIB2 (такие файлы обычно имеют расширение «.smt2»). Инструмент LiquidHaskell реализует ссылку Верификатор на основе типа элемента для Haskell, который может использовать любой совместимый с SMTLIB2 решатель, например CVC4, MathSat или Z3.

Анализ и тестирование на основе символьного исполнения

Важным применением решателей SMT является символьное выполнение для анализа и тестирования программ (например, concolic testing ), направленный, в частности, на поиск уязвимостей безопасности. К важным активно поддерживаемым инструментам в этой категории относятся SAGE из Microsoft Research, KLEE, S2E и Triton.. Решатели SMT, которые особенно полезны для приложений с символьным исполнением, включают Z3, STP, Z3str2 и Boolector.

• Программирование набора ответов
• Автоматическое доказательство теорем

1. ^Barbosa, Haniel, et al. "Расширение решателей SMT до логики более высокого порядка." Международная конференция по автоматическому отчислению. Springer, Cham, 2019.
2. ^Nieuwenhuis, R.; Oliveras, A.; Тинелли, С. (2006), "Решение теорий SAT и SAT по модулю: от абстрактной процедуры Дэвиса-Патнэма-Логеманна-Ловленда до DPLL (T)", Журнал ACM (PDF), 53, pp. 937–977
3. ^Bauer, A.; Пистер, М.; Таучниг, М. (2007), «Инструментальная поддержка для анализа гибридных систем и моделей», Труды конференции 2007 года по проектированию, автоматизации и тестированию в Европе (DATE'07), IEEE Computer Society, стр. 1, CiteSeerX 10.1.1.323.6807, doi : 10.1109 / DATE.2007.364411, ISBN 978-3-9810801-2-4, S2CID 9159847
4. ^Fränzle, M.; Herde, C.; Ratschan, S.; Schubert, T.; Тейдж, Т. (2007), «Эффективное решение больших нелинейных систем арифметических ограничений со сложной логической структурой», Специальный выпуск JSAT по интеграции SAT / CP (PDF), 1, стр. 209–236
5. ^Барретт, Кларк; де Моура, Леонардо; Пень, Аарон (2005). Этессами, Коуша; Раджамани, Шрирам К. (ред.). "SMT-COMP: Конкурс теорий удовлетворенности по модулю". Компьютерная проверка. Конспект лекций по информатике. Берлин, Гейдельберг: Springer: 20–23. doi : 10.1007 / 11513988_4. ISBN 978-3-540-31686-2.
6. ^Барретт, Кларк; де Моура, Леонардо; Ранис, Сильвио; Пень, Аарон; Тинелли, Чезаре (2011). Барнер, Шэрон; Харрис, Ян; Кронинг, Даниэль; Раз, Орна (ред.). «Инициатива SMT-LIB и рост SMT». Аппаратное и программное обеспечение: проверка и тестирование. Конспект лекций по информатике. Берлин, Гейдельберг: Springer: 3–3. DOI : 10.1007 / 978-3-642-19583-9_2. ISBN 978-3-642-19583-9.
7. ^«SMT-COMP 2020». SMT-COMP. Проверено 19 октября 2020 г.
8. ^Бомонт, Пол; Эванс, Нил; Хут, Майкл; Завод, Том (2015). Пернул, Гюнтер; Y. Райан, Питер; Weippl, Эдгар (ред.). «Анализ уверенности для контроля над ядерным оружием: SMT-абстракции байесовских сетей верований». Компьютерная безопасность - ESORICS 2015. Конспект лекций по информатике. Чам: Издательство Springer International: 521–540. DOI : 10.1007 / 978-3-319-24174-6_27. ISBN 978-3-319-24174-6.

• С. Барретт, Р. Себастьяни, С. Сешиа, С. Тинелли, «Теории выполнимости по модулю. " В Справочнике по выполнимости, т. 185 of Frontiers in Artificial Intelligence and Applications, (A Biere, MJH Heule, H van Maaren, and T. Walsh, ред.), IOS Press, февраль 2009 г., стр. 825–885.
• Виджай Ганеш ( PhD. Thesis 2007), Процедуры принятия решений для битовых векторов, массивов и целых чисел, факультет компьютерных наук, Стэнфордский университет, Стэнфорд, Калифорния, США, сентябрь 2007 г.
• Susmit Jha, Rhishikesh Limaye, и Санджит А. Сешия. Бивер: разработка эффективного решателя SMT для бит-векторной арифметики. В материалах 21-й Международной конференции по компьютерной проверке, стр. 668–674, 2009.
• R. Э. Брайант, С. М. Герман и М. Н. Велев, «Проверка микропроцессора с использованием эффективных процедур принятия решений для логики равенства с неинтерпретируемыми функциями », в Аналитических таблицах и связанных с ними методах, стр. 1–13, 1999.
• М. Дэвис и Х. Патнэм, Вычислительная процедура для теории количественной оценки, Журнал Ассоциации вычислительной техники, вып. 7, no., Pp. 201–215, 1960.
• М. Дэвис, Дж. Логеманн и Д. Ловленд, Машинная программа для доказательства теорем, Связь ACM, т. 5, вып. 7. С. 394–397, 1962.
• Д. Кроенинг и О. Стрихман, Процедуры принятия решений - алгоритмическая точка зрения (2008), Springer (серия теоретической информатики) ISBN 978-3-540- 74104-6.
• Г.-Дж. Нам, К. А. Сакаллах, Р. Рутенбар, Новый подход к детальной маршрутизации ПЛИС с помощью логической удовлетворенности на основе поиска, Транзакции IEEE по автоматизированному проектированию интегральных схем и систем, т. 21, нет. 6, pp. 674–684, 2002.
• SMT-LIB: Библиотека теорий по модулю соответствия
• SMT-COMP: Конкурс теорий по модулю удовлетворенности
• Процедуры принятия решений - алгоритмическая точка зрения
• R. Sebastiani, Lazy Satisfiability Modulo Theories, Dipartimento di Ingegneria e Scienza dell'Informazione, Universita di Trento, Италия, декабрь 2007 г.
• Д.Юричев, Краткое введение в решатели SAT / SMT и символическое исполнение

Эта статья адаптирована из столбца электронного информационного бюллетеня ACM SIGDA , подготовленного проф. Карем Сакаллах. Исходный текст доступен здесь