В информатике и математической логике , то выполнимость по модулю теория ( SMT ) проблема является проблемой решения для логических формул относительно комбинаций фоновых теорий , выраженных в классической логике первого порядка с равенством. Примерами теорий, обычно используемых в информатике, являются теория действительных чисел , теория целых чисел и теории различных структур данных, таких как списки , массивы , битовые векторы и т. Д. SMT можно рассматривать как формупроблема удовлетворения ограничений и, следовательно, некий формализованный подход к программированию ограничений .
Формально говоря, экземпляр SMT - это формула в логике первого порядка , где некоторые функции и символы предиката имеют дополнительные интерпретации, а SMT - это проблема определения выполнимости такой формулы. Другими словами, представьте себе пример проблемы логической выполнимости (SAT), в которой некоторые из двоичных переменных заменяются предикатами для подходящего набора небинарных переменных. Предикат - это двоичная функция недвоичных переменных. Примеры предикатов включают линейные неравенства (например, ) или равенства, включающие неинтерпретированные термины и функциональные символы (например, где- некоторая неопределенная функция двух аргументов). Эти предикаты классифицируются согласно каждой присвоенной теории. Например, линейные неравенства над действительными переменными оцениваются с использованием правил теории линейной вещественной арифметики , тогда как предикаты, включающие неинтерпретированные термины и функциональные символы, оцениваются с использованием правил теории неинтерпретируемых функций с равенством (иногда называемой пустой теорией ). Другие теории включают теории массивов и структур списков (полезны для моделирования и проверки компьютерных программ ) и теорию битовых векторов (полезны при моделировании и проверкеаппаратные конструкции ). Также возможны подтеории: например, разностная логика - это подтеория линейной арифметики, в которой каждое неравенство ограничено, чтобы иметь форму для переменных и и константы .
Большинство решателей SMT поддерживают только бескванторные фрагменты своей логики.
Экземпляр SMT - это обобщение логического экземпляра SAT, в котором различные наборы переменных заменяются предикатами из множества лежащих в основе теорий. Формулы SMT предоставляют гораздо более богатый язык моделирования, чем это возможно с булевыми формулами SAT. Например, формула SMT позволяет нам моделировать операции канала данных микропроцессора на уровне слова, а не на уровне битов.
Для сравнения, программирование набора ответов также основано на предикатах (точнее, на атомарных предложениях, созданных из атомарной формулы ). В отличие от SMT, программы с набором ответов не имеют кванторов и не могут легко выразить ограничения, такие как линейная арифметика или разностная логика - ASP в лучшем случае подходит для булевых задач, которые сводятся к свободной теории неинтерпретируемых функций. Реализация 32-битных целых чисел в качестве битовых векторов в ASP страдает от большинства проблем, с которыми сталкивались ранние решатели SMT: «очевидные» идентичности, такие как x + y = y + x , трудно вывести.
Программирование с логикой ограничений действительно обеспечивает поддержку линейных арифметических ограничений, но в совершенно другой теоретической структуре. [ необходима цитата ] Решатели SMT также были расширены для решения формул в логике более высокого порядка . [1]
Ранние попытки решения экземпляров SMT включали преобразование их в логические экземпляры SAT (например, 32-битная целочисленная переменная будет кодироваться 32 однобитными переменными с соответствующими весами, а операции на уровне слова, такие как `` плюс '', будут заменены на более низкие - логические операции уровня над битами) и передать эту формулу логическому вычислителю SAT. Этот подход, который упоминается как в нетерпеливого подходе, имеет свои достоинства: путем предварительной обработки формулы SMT в эквивалентную булеву формулу SAT существующие булевы решатели SAT могут использоваться «как есть», а их производительность и емкость улучшаются с течением времени. С другой стороны, потеря высокоуровневой семантики лежащих в основе теорий означает, что логическая программа расчета SAT должна работать намного усерднее, чем необходимо, чтобы обнаружить "очевидные" факты (например, для сложения целых чисел). Это наблюдение привело к разработка ряда решателей SMT, которые тесно интегрируют логические рассуждения о поиске в стиле DPLL с решателями, специфичными для теории ( T-решатели ), которые обрабатывают конъюнкции (AND) предикатов из данной теории. Такой подход называется ленивымподход .
Дублированный DPLL (Т) , [2] эта архитектура дает ответственность булевых рассуждений на основе DPLL SAT решатель , который, в свою очередь, взаимодействует с решателем для теории T через хорошо определенный интерфейс. Решателю теории нужно беспокоиться только о проверке выполнимости конъюнкций предикатов теории, переданных ему из решателя SAT, когда он исследует булево пространство поиска формулы. Однако для того, чтобы эта интеграция работала хорошо, решатель теории должен иметь возможность участвовать в распространении и анализе конфликтов, т. Е. Он должен иметь возможность выводить новые факты из уже установленных фактов, а также давать краткие объяснения неосуществимости, когда теория противоречит возникают. Другими словами, решатель теории должен быть инкрементным и иметь возможность обратного отслеживания .
Большинство общих подходов к SMT поддерживают разрешимые теории. Однако многие системы реального мира можно смоделировать только с помощью нелинейной арифметики над действительными числами, включая трансцендентные функции , например самолет и его поведение. Этот факт побуждает распространить проблему SMT на нелинейные теории, например, определить, следует ли
куда
выполнимо. Тогда такие проблемы вообще становятся неразрешимыми . (Теория вещественных замкнутых полей и, следовательно, полная теория действительных чисел первого порядка , однако, разрешимы с использованием исключения кванторов . Это сделано Альфредом Тарским .) Теория натуральных чисел первого порядка со сложением (но не умножением) , называемая арифметикой Пресбургера , также разрешима. Поскольку умножение на константы может быть реализовано как вложенное сложение, арифметика во многих компьютерных программах может быть выражена с помощью арифметики Пресбургера, что приводит к разрешимым формулам.
Примерами решателей SMT, обращающимися к булевым комбинациям атомов теории из неразрешимых арифметических теорий над действительными числами, являются ABsolver [3], в котором используется классическая архитектура DPLL (T) с пакетом нелинейной оптимизации в качестве (обязательно неполного) решателя теории подчиненных функций, и iSAT , основанный на объединении DPLL SAT-решения и распространения интервальных ограничений, называемый алгоритмом iSAT. [4]
В таблице ниже приведены некоторые функции многих доступных решателей SMT. Столбец «SMT-LIB» указывает совместимость с языком SMT-LIB; многие системы, отмеченные «да», могут поддерживать только старые версии SMT-LIB или предлагать только частичную поддержку языка. Столбец «CVC» указывает на поддержку языка CVC. Столбец «DIMACS» указывает на поддержку формата DIMACS .
Проекты различаются не только функциями и производительностью, но и жизнеспособностью окружающего сообщества, его постоянным интересом к проекту и его способностью вносить документацию, исправления, тесты и улучшения.
Платформа | Функции | Примечания | |||||||
---|---|---|---|---|---|---|---|---|---|
Имя | Операционные системы | Лицензия | SMT-LIB | CVC | DIMACS | Встроенные теории | API | SMT-COMP [1] | |
ABsolver | Linux | CPL | v1.2 | Нет | да | линейная арифметика, нелинейная арифметика | C ++ | нет | На основе DPLL |
Альт-Эрго | Linux , Mac OS , Windows | CeCILL-C (примерно эквивалент LGPL ) | частичные v1.2 и v2.0 | Нет | Нет | пустая теория , линейное целое и рациональный арифметик, нелинейные арифметический, полиморфные массивы , перечисленные типов данных , символы переменного тока , битвекторы , запись типов данных , кванторы | OCaml | 2008 г. | Полиморфный язык ввода первого порядка а-ля ML, основанный на SAT-решателе, объединяет подходы типа Шостака и Нельсона-Оппена для рассуждения теорий по модулю |
Barcelogic | Linux | Проприетарный | v1.2 | пустая теория , логика различия | C ++ | 2009 г. | Закрытие конгруэнтности на основе DPLL | ||
Бобр | Linux , Windows | BSD | v1.2 | Нет | Нет | битвекторы | OCaml | 2009 г. | На основе SAT-решателя |
Булектор | Linux | Массачусетский технологический институт | v1.2 | Нет | Нет | битовые векторы , массивы | C | 2009 г. | На основе SAT-решателя |
CVC3 | Linux | BSD | v1.2 | да | пустая теория , линейная арифметика, массивы, кортежи, типы, записи, битовые векторы, кванторы | C / C ++ | 2010 г. | вывод доказательства в HOL | |
CVC4 | Linux , Mac OS , Windows , FreeBSD | BSD | да | да | рациональная и целочисленная линейная арифметика, массивы, кортежи, записи, индуктивные типы данных, битовые векторы, строки и равенство над неинтерпретируемыми функциональными символами | C ++ | 2010 г. | версия 1.5 выпущена в июле 2017 г. | |
Инструментарий процедуры принятия решений (DPT) | Linux | Apache | Нет | OCaml | нет | На основе DPLL | |||
Я сидел | Linux | Проприетарный | Нет | нелинейная арифметика | нет | На основе DPLL | |||
MathSAT | Linux , Mac OS , Windows | Проприетарный | да | да | пустая теория , линейная арифметика, нелинейная арифметика, битовые векторы, массивы | C / C ++ , Python , Java | 2010 г. | На основе DPLL | |
MiniSmt | Linux | LGPL | частичная v2.0 | нелинейная арифметика | 2010 г. | На основе SAT-решателя, на основе Yices | |||
Норн | Решатель SMT для строковых ограничений | ||||||||
OpenCog | Linux | AGPL | Нет | Нет | Нет | вероятностная логика , арифметика. реляционные модели | C ++ , Схема , Python | нет | изоморфизм подграфов |
OpenSMT | Linux , Mac OS , Windows | GPLv3 | частичная v2.0 | да | пустая теория , разности, линейная арифметика, битовые векторы | C ++ | 2011 г. | ленивый SMT Solver | |
расат | Linux | GPLv3 | v2.0 | действительная и целочисленная нелинейная арифметика | 2014, 2015 | Расширение распространения интервальных ограничений с помощью тестирования и теоремы о промежуточном значении | |||
Сатин | ? | Проприетарный | v1.2 | линейная арифметика, разностная логика | никто | 2009 г. | |||
СМТИнтерпол | Linux , Mac OS , Windows | LGPLv3 | v2.5 | неинтерпретируемые функции, линейная вещественная арифметика и линейная целочисленная арифметика | Джава | 2012 г. | Ориентирован на создание высококачественных компактных интерполянтов. | ||
СМЧР | Linux , Mac OS , Windows | GPLv3 | Нет | Нет | Нет | линейная арифметика, нелинейная арифметика, кучи | C | нет | Может реализовывать новые теории с помощью правил обработки ограничений . |
SMT-RAT | Linux , Mac OS | Массачусетский технологический институт | v2.0 | Нет | Нет | линейная арифметика, нелинейная арифметика | C ++ | 2015 г. | Набор инструментов для стратегического и параллельного решения SMT, состоящий из набора совместимых с SMT реализаций. |
SONOLAR | Linux , Windows | Проприетарный | частичная v2.0 | битвекторы | C | 2010 г. | На основе SAT-решателя | ||
Копье | Linux , Mac OS , Windows | Проприетарный | v1.2 | битвекторы | 2008 г. | ||||
STP | Linux , OpenBSD , Windows , Mac OS | Массачусетский технологический институт | частичная v2.0 | да | Нет | битовые векторы, массивы | C , C ++ , Python , OCaml , Java | 2011 г. | На основе SAT-решателя |
МЕЧ | Linux | Проприетарный | v1.2 | битвекторы | 2009 г. | ||||
UCLID | Linux | BSD | Нет | Нет | Нет | пустая теория , линейная арифметика, битовые векторы и ограниченная лямбда (массивы, память, кеш и т. д.) | нет | На основе SAT-решателя, написанного на московском ML . Язык ввода - проверка модели SMV. Хорошо задокументированы! | |
верит | Linux , OS X | BSD | частичная v2.0 | пустая теория , рациональная и целочисленная линейная арифметика, кванторы и равенство по неинтерпретированным функциональным символам | C / C ++ | 2010 г. | На основе SAT-решателя | ||
Yices | Linux , Mac OS , Windows , FreeBSD | GPLv3 | v2.0 | Нет | да | рациональная и целочисленная линейная арифметика, битовые векторы, массивы и равенство по неинтерпретированным функциональным символам | C | 2014 г. | Исходный код доступен онлайн |
Z3 Доказательство теорем | Linux , Mac OS , Windows , FreeBSD | Массачусетский технологический институт | v2.0 | да | пустая теория , линейная арифметика, нелинейная арифметика, битовые векторы, массивы, типы данных, кванторы , строки | C / C ++ , .NET , OCaml , Python , Java , Haskell | 2011 г. | Исходный код доступен онлайн |
Есть несколько попыток описать стандартизованный интерфейс для решателей SMT (и автоматических средств доказательства теорем , термин, часто используемый как синоним). Самым известным из них является стандарт SMT-LIB, [ цитата необходима ], который предоставляет язык, основанный на S-выражениях . Другие обычно поддерживаемые стандартизованные форматы - это формат DIMACS [ необходима ссылка ], поддерживаемый многими логическими программами SAT, и формат CVC [ требуется ссылка ], используемый автоматическим средством доказательства теорем CVC.
Формат SMT-LIB также поставляется с рядом стандартизированных тестов и позволяет проводить ежегодное соревнование между решателями SMT под названием SMT-COMP. Первоначально конкурс проводился во время конференции по компьютерной проверке (CAV), [5] [6], но с 2020 года конкурс проводится в рамках семинара SMT, который является аффилированным лицом Международной объединенной конференции по автоматизированному мышлению (IJCAR). ). [7]
Решатели SMT полезны как для проверки, доказательства правильности программ, тестирования программного обеспечения, основанного на символьном исполнении , так и для синтеза , генерации фрагментов программы путем поиска в пространстве возможных программ. Помимо верификации программного обеспечения, решатели SMT также использовались для вывода типов [8] [9] и для моделирования теоретических сценариев, включая моделирование убеждений участников в контроле над ядерными вооружениями . [10]
Для компьютерной проверки компьютерных программ часто используются решатели SMT. Распространенным методом является перевод предусловий, постусловий, условий цикла и утверждений в формулы SMT, чтобы определить, все ли свойства могут выполняться.
Есть много верификаторов, построенных на основе решателя Z3 SMT . Boogie - это язык промежуточной проверки, который использует Z3 для автоматической проверки простых императивных программ. VCC верификатор для одновременного C использует буги, а также Dafny для императивных объектно-ориентированных программ, Чашу для параллельных программ, и Spec # для C #. F * - это язык с зависимой типизацией, использующий Z3 для поиска доказательств; компилятор передает эти доказательства для создания байт-кода, несущего доказательство. Проверка Гадюка инфраструктура кодирует проверки условия для Z3. ЗСОБиблиотека обеспечивает проверку программ Haskell на основе SMT и позволяет пользователю выбирать среди ряда решателей, таких как Z3, ABC, Boolector, CVC4 , MathSAT и Yices.
Также существует множество верификаторов, построенных на основе решателя Alt-Ergo SMT. Вот список зрелых приложений:
Многие решатели SMT реализуют общий формат интерфейса, называемый SMTLIB2 (такие файлы обычно имеют расширение « .smt2 »). Инструмент LiquidHaskell реализует верификатор на основе типа уточнения для Haskell, который может использовать любой совместимый с SMTLIB2 решатель, например CVC4, MathSat или Z3.
Важным применением решателей SMT является символьное выполнение для анализа и тестирования программ (например, тестирование concolic ), нацеленных, в частности, на обнаружение уязвимостей безопасности. К важным активно поддерживаемым инструментам в этой категории относятся SAGE от Microsoft Research , KLEE , S2E и Triton . Решатели SMT, которые особенно полезны для приложений с символьным исполнением, включают Z3 , STP , Z3str2 и Boolector .
Эта статья адаптирована из колонки в электронном информационном бюллетене ACM SIGDA, подготовленной профессором Каремом Сакаллахом . Исходный текст доступен здесь