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

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

Основная терминология

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

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

Выразительная сила

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

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

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

Подходы решателя

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

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

SMT для неразрешимых теорий

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

{\ displaystyle {\ begin {array} {lr} & (\ sin (x) ^ {3} = \ cos (\ log (y) \ cdot x) \ vee b \ vee -x ^ {2} \ geq 2.3 y) \ wedge \ left (\ neg b \ vee y <-34,4 \ vee \ exp (x)> {y \ over x} \ right) \ end {array}}}

где

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

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

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

Решатели

В таблице ниже приведены некоторые функции многих доступных решателей 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-COMP

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

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

Приложения

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

Проверка

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

Есть много верификаторов, построенных на основе решателя Z3 SMT . Boogie - это язык промежуточной проверки, который использует Z3 для автоматической проверки простых императивных программ. VCC верификатор для одновременного C использует буги, а также Dafny для императивных объектно-ориентированных программ, Чашу для параллельных программ, и Spec # для C #. F * - это язык с зависимой типизацией, использующий Z3 для поиска доказательств; компилятор передает эти доказательства для создания байт-кода, несущего доказательство. Проверка Гадюка инфраструктура кодирует проверки условия для 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 .

Смотрите также

Заметки

^ Барбоза, Ханиэль и др. « Расширение решателей SMT до логики более высокого порядка ». Международная конференция по автоматическому отчислению. Спрингер, Чам, 2019.
^ Nieuwenhuis, R .; Oliveras, A .; Тинелли, К. (2006), "Решение теорий SAT и SAT по модулю: от абстрактной процедуры Дэвиса-Патнэма-Логеманна-Ловленда до DPLL (T)", Журнал ACM (PDF) , 53 , стр. 937–977
^ Бауэр, А .; Пистер, М .; Tautschnig, M. (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
^ Fränzle, M .; Herde, C .; Ratschan, S .; Шуберт, Т .; Тейдж, Т. (2007), "Эффективное решение больших нелинейных арифметических систем ограничений со сложной булевой структурой", Специальный выпуск JSAT по интеграции SAT / CP (PDF) , 1 , стр. 209–236
^ Барретт, Кларк; де Моура, Леонардо; Пень, Аарон (2005). Этессами, Коуша; Раджамани, Шрирам К. (ред.). "SMT-COMP: Конкурс теорий выполнимости по модулю" . Компьютерная проверка . Конспект лекций по информатике. Берлин, Гейдельберг: Springer: 20–23. DOI : 10.1007 / 11513988_4 . ISBN 978-3-540-31686-2.
^ Барретт, Кларк; де Моура, Леонардо; Ранис, Сильвио; Пень, Аарон; Тинелли, Чезаре (2011). Барнер, Шэрон; Харрис, Ян; Кронинг, Даниэль; Раз, Орна (ред.). «Инициатива SMT-LIB и рост SMT» . Аппаратное и программное обеспечение: проверка и тестирование . Конспект лекций по информатике. Берлин, Гейдельберг: Springer: 3–3. DOI : 10.1007 / 978-3-642-19583-9_2 . ISBN 978-3-642-19583-9.
^ "SMT-COMP 2020" . SMT-COMP . Проверено 19 октября 2020 .
^ Хасан, Мостафа и др. "Вывод типа на основе Maxsmt для python 3." Международная конференция по компьютерной проверке. Спрингер, Чам, 2018.
^ Loncaric, Calvin, et al. «Практическая основа для объяснения ошибок вывода типов». Уведомления ACM SIGPLAN 51.10 (2016): 781-799.
^ Бомонт, Пол; Эванс, Нил; Хут, Майкл; Завод, Том (2015). Пернул, Гюнтер; Я. Райан, Питер; Weippl, Эдгар (ред.). "Анализ уверенности для контроля над ядерным оружием: SMT-абстракции байесовских сетей верований" . Компьютерная безопасность - ESORICS 2015 . Конспект лекций по информатике. Чам: Издательство Springer International: 521–540. DOI : 10.1007 / 978-3-319-24174-6_27 . ISBN 978-3-319-24174-6.

Languages

In other projects