Теории выполнимости по модулю

В информатике и математической логике теория выполнимости по модулю SMT ) представляет собой проблему определения математической формулы выполнимости . ( Он обобщает проблему логической выполнимости (SAT) на более сложные формулы, включающие действительные числа , целые числа и/или различные структуры данных , такие как списки , массивы , битовые векторы и строки . Название происходит от того факта, что эти выражения интерпретируются в рамках («по модулю») определенной формальной теории в логике первого порядка с равенством (часто без учета кванторов ). Решатели SMT — это инструменты, целью которых является решение проблемы SMT для практического подмножества входных данных. Решатели SMT, такие как Z3 и cvc5, использовались в качестве строительного блока для широкого спектра приложений в области информатики, в том числе для автоматического доказательства теорем , анализа программ , проверки программ и тестирования программного обеспечения .

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

Терминология и примеры

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

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

Выполнимость: Определите, если $x\vee (y\wedge \neg z)$ является удовлетворительным.
Доступ к массиву: найти значение для массиватакой, что A[0]=5.
Арифметика битовых векторов: определите, являются ли x и y разными 3-битными числами.
Неинтерпретируемые функции: найдите значения x и y такие, что $f(x)=2$ и $g(x)=3$ .

Большинство решателей SMT поддерживают только кванторов . фрагменты своей логики, не содержащие ^{[ нужна ссылка ]}

Связь с автоматизированным доказательством теорем

Существует существенное совпадение между решением SMT и автоматизированным доказательством теорем . Как правило, автоматизированные средства доказательства теорем сосредотачиваются на поддержке полной логики первого порядка с помощью кванторов, тогда как средства решения SMT больше сосредотачиваются на поддержке различных теорий (интерпретируемых символов предикатов). ATP превосходно справляются с задачами с большим количеством кванторов, тогда как решатели SMT хорошо справляются с большими задачами без кванторов. ^[1] Граница настолько размыта, что некоторые ATP участвуют в SMT-COMP, а некоторые решатели SMT участвуют в CASC . ^[2]

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

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

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

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

Решающие подходы

Ранние попытки решения примеров SMT включали их преобразование в логические экземпляры SAT (например, 32-битная целочисленная переменная кодировалась 32 однобитовыми переменными с соответствующими весами, а операции на уровне слов, такие как «плюс», заменялись более низкими значениями). логические операции над битами) и передачу этой формулы логическому решателю SAT. Этот подход, который называется нетерпеливым ), имеет свои преимущества: путем предварительной обработки формулы SMT в эквивалентную логическую формулу SAT существующие решатели Boolean SAT могут использоваться «как есть», а их производительность и мощность могут быть использованы « как подходом (или побитовой очисткой есть». улучшения, полученные с течением времени. С другой стороны, потеря высокоуровневой семантики лежащих в основе теорий означает, что логическому решателю SAT приходится работать намного усерднее, чем необходимо, чтобы обнаружить «очевидные» факты (такие как $x+y=y+x$ для сложения целых чисел.) Это наблюдение привело к разработке ряда решателей SMT, которые тесно интегрируют логические рассуждения поиска в стиле DPLL с решателями, специфичными для теории ( T-солверами ), которые обрабатывают соединения (И) предикатов из заданного числа. теория. подход называется ленивым . подходом Этот ^[4]

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

Разрешимые теории

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

Другое направление исследований включает разработку специализированных разрешимых теорий , включая линейную арифметику над рациональными и целыми числами , битвекторы фиксированной ширины, ^[7] арифметика с плавающей запятой (часто реализуется в решателях SMT посредством побитовой обработки , т. е. приведения к битовым векторам), ^[8]^[9] струны , ^[10] (co)-типы данных , ^[11] последовательности (используются для моделирования динамических массивов ), ^[12] конечные множества и отношения , ^[13]^[14] логика разделения , ^[15] конечные поля , ^[16] и неинтерпретированные функции среди прочего.

Булевы монотонные теории — это класс теорий, которые поддерживают эффективное распространение теории и анализ конфликтов, что позволяет их практическое использование в решателях DPLL(T). ^[17] Монотонные теории поддерживают только логические переменные (единственный сорт — логические ), и все их функции и предикаты $p$ подчиняются аксиоме

$p(\ldots ,b_{i-1},0,b_{i+1},\ldots )\implies p(\ldots ,b_{i-1},1,b_{i+1},\ldots )$

Примеры монотонных теорий включают достижимость графа , обнаружение столкновений для выпуклых оболочек , минимальные разрезы и логику дерева вычислений . ^[18] Любую программу Datalog можно интерпретировать как монотонную теорию. ^[19]

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

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

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

где

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

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

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

Решатели

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

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

Платформа			Функции						Примечания
Имя	ТЫ	Лицензия	СМТ-ЛИБ	КВК	ДИМАКС	Встроенные теории	API	СМТ-КОМП [1]
Оправдать	Линукс	CPL	v1.2	Нет	Да	линейная арифметика, нелинейная арифметика	С++	нет	на базе DPLL
Альт-Эрго	Linux , Mac OS , Windows	CeCILL-C (примерно эквивалент LGPL )	частичная версия 1.2 и версия 2.0	Нет	Нет	пустая теория , линейная целочисленная и рациональная арифметика, нелинейная арифметика, полиморфные массивы , перечислимые типы данных , AC-символы , битовые векторы , типы данных записи , кванторы	OCaml	2008	Полиморфный язык ввода первого порядка в стиле ML, основанный на SAT-решателе, сочетает в себе подходы типа Шостака и Нельсона-Оппена для рассуждения теорий по модулю.
Барселоджик	Линукс	Собственный	v1.2			пустая теория , разностная логика	С++	2009	на основе DPLL Замыкание конгруэнтности
Бобр	Линукс , Винда	БСД	v1.2	Нет	Нет	битвекторы	OCaml	2009	на базе SAT-солвера
Булектор	Линукс	С	v1.2	Нет	Нет	битвекторы , массивы	С	2009	на базе SAT-солвера
CVC3	Линукс	БСД	v1.2	Да		пустая теория , линейная арифметика, массивы, кортежи, типы, записи, битвекторы, кванторы	С / С++	2010	вывод доказательства в HOL
CVC4	Linux , Mac OS , Windows , FreeBSD	БСД	Да	Да		рациональная и целочисленная линейная арифметика, массивы, кортежи, записи, индуктивные типы данных, битовые векторы, строки и равенство неинтерпретируемых функциональных символов.	С++	2021	версия 1.8 выпущена в мае 2021 г.
cvc5	Linux , Mac OS , Windows	БСД	Да	Да		рациональная и целочисленная линейная арифметика, массивы, кортежи, записи, индуктивные типы данных, битовые векторы, строки, последовательности, пакеты и равенство неинтерпретируемых функциональных символов.	С++, Питон, Ява	2021	версия 1.0 выпущена в апреле 2022 г.
Инструментарий процедуры принятия решения (DPT)	Линукс	Апач	Нет				OCaml	нет	на базе DPLL
iSAT	Линукс	Собственный	Нет			нелинейная арифметика		нет	на базе DPLL
МатСАТ	Linux , Mac OS , Windows	Собственный	Да		Да	пустая теория , линейная арифметика, нелинейная арифметика, битвекторы, массивы	Си / С++ , Питон , Ява	2010	на базе DPLL
МиниСмт	Линукс	LGPL	частичная версия 2.0			нелинейная арифметика	OCaml	2010	На основе SAT-солвера, на основе Yices
Ведьма									SMT-решатель для строковых ограничений
OpenCog	Линукс	АГПЛ	Нет	Нет	Нет	вероятностная логика , арифметика. реляционные модели	C++ , Схема , Питон	нет	изоморфизм подграфов
ОпенСМТ	Linux , Mac OS , Windows	лицензия GPLv3	частичная версия 2.0		Да	пустая теория , разности, линейная арифметика, битвекторы	С++	2011	ленивый SMT-решатель
raSAT	Линукс	лицензия GPLv3	v2.0			действительная и целочисленная нелинейная арифметика		2014, 2015	расширение интервального распространения ограничений с помощью тестирования и теоремы о промежуточном значении
Сатин	?	Собственный	v1.2			линейная арифметика, разностная логика	никто	2009
СМТИнтерпол	Linux , Mac OS , Windows	LGPLv3	v2.5			неинтерпретируемые функции, линейная действительная арифметика и линейная целочисленная арифметика	Ява	2012	Основное внимание уделяется созданию высококачественных компактных интерполянтов.
СМЧР	Linux , Mac OS , Windows	лицензия GPLv3	Нет	Нет	Нет	линейная арифметика, нелинейная арифметика, кучи	С	нет	Может реализовывать новые теории, используя правила обработки ограничений .
СМТ-РАТ	Линукс , МакОС	С	v2.0	Нет	Нет	линейная арифметика, нелинейная арифметика	С++	2015	Набор инструментов для стратегических и параллельных решений SMT, состоящий из набора реализаций, совместимых с SMT.
СОНОЛАР	Линукс , Винда	Собственный	частичная версия 2.0			битвекторы	С	2010	на базе SAT-солвера
Копье	Linux , Mac OS , Windows	Собственный	v1.2			битвекторы		2008
СТП	Linux , OpenBSD , Windows , Mac OS	С	частичная версия 2.0	Да	Нет	битовые векторы, массивы	C , C++ , Python , OCaml , Java	2011	на базе SAT-солвера
МЕЧ	Линукс	Собственный	v1.2			битвекторы		2009
УКЛИД	Линукс	БСД	Нет	Нет	Нет	пустая теория , линейная арифметика, битвекторы и ограниченная лямбда (массивы, память, кеш и т. д.)		нет	На базе SAT-солвера, написанного в Москве ML . Язык ввода — средство проверки модели SMV. Хорошо документировано!
veriT	Линукс , ОС Х	БСД	частичная версия 2.0			пустая теория , рациональная и целочисленная линейная арифметика, кванторы и равенство неинтерпретируемых функциональных символов	С / С++	2010	На основе SAT-решателя, может предоставлять доказательства
Йайс	Linux , Mac OS , Windows , FreeBSD	лицензия GPLv3	v2.0	Нет	Да	рациональная и целочисленная линейная арифметика, битовые векторы, массивы и равенство неинтерпретируемых функциональных символов.	С	2014	Исходный код доступен в Интернете.
Теорема Z3	Linux , Mac OS , Windows , FreeBSD	С	v2.0		Да	пустая теория , линейная арифметика, нелинейная арифметика, битовые векторы, массивы, типы данных, кванторы , строки	C / C++ , .NET , OCaml , Python , Java , Haskell	2011	Исходный код доступен в Интернете.

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

Существует множество попыток описать стандартизированный интерфейс для решателей SMT (и автоматизированных средств доказательства теорем — термин, часто используемый как синоним). Наиболее известным является стандарт SMT-LIB. ^{[ нужна ссылка ]} который предоставляет язык, основанный на S-выражениях . Другими обычно поддерживаемыми стандартизированными форматами являются формат DIMACS. ^{[ нужна ссылка ]} поддерживается многими решателями Boolean SAT и форматом CVC ^{[ нужна ссылка ]} используется автоматическим средством доказательства теорем CVC.

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

Приложения

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

Проверка

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

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

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

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

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

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

Важным применением решателей SMT является символьное выполнение для анализа и тестирования программ (например, concolic-тестирование ), направленного, в частности, на поиск уязвимостей безопасности. ^{[ нужна ссылка ]} Примеры инструментов этой категории включают SAGE от Microsoft Research , KLEE , S2E и Triton . Решатели SMT, которые использовались для приложений символьного выполнения, включают Z3 , STP, архивировано 6 апреля 2015 г. на Wayback Machine , семейство решателей Z3str и Boolector . ^{[ нужна ссылка ]}

Интерактивное доказательство теорем

Решатели SMT были интегрированы с помощниками по проверке, включая Coq. ^[29] и Изабель/ХОЛ . ^[30]

См. также

Примечания

^ Бланшетт, Жасмин Кристиан; Бёме, Саша; Полсон, Лоуренс К. (01 июня 2013 г.). «Расширение кувалды с помощью решателей SMT» . Журнал автоматизированного рассуждения . 51 (1): 109–128. дои : 10.1007/s10817-013-9278-5 . ISSN 1573-0670 . Решатели ATP и SMT имеют взаимодополняющие преимущества. Первые более элегантно справляются с квантификаторами, тогда как вторые превосходно справляются с большими, в основном наземными задачами.
^ Вебер, Тьярк; Коншон, Сильвен; Дехарб, Давид; Хейцманн, Матиас; Нимец, Айна; Регер, Джайлз (01 января 2019 г.). «Конкурс СМТ 2015–2018» . Журнал по выполнимости, логическому моделированию и вычислениям . 11 (1): 221–259. дои : 10.3233/SAT190123 . S2CID 210147712 . В последние годы мы наблюдаем стирание границ между SMT-COMP и CASC: решатели SMT конкурируют в CASC, а ATP — в SMT-COMP.
^ Барбоза, Ханиэль; Рейнольдс, Эндрю; Эль Урауи, Дэниел; Тинелли, Чезаре; Барретт, Кларк (2019). «Расширение решателей SMT на логику высшего порядка» . Автоматический дедукция – CADE 27: 27-я Международная конференция по автоматическому дедукции, Натал, Бразилия, 27–30 августа 2019 г., Материалы . Спрингер. стр. 35–54. дои : 10.1007/978-3-030-29436-6_3 . ISBN 978-3-030-29436-6 . S2CID 85443815 . hal-02300986.
^ Бруттомессо, Роберто; Чиматти, Алессандро; Франзен, Андерс; Гриджио, Альберто; Ханна, Зияд; Надель, Александр; Палти, Амит; Себастьяни, Роберто (2007). «Ленивый и многоуровневый SMT($\mathcal{BV}$) решатель для сложных задач промышленной верификации» . В Дамме, Вернер; Германнс, Хольгер (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 4590. Берлин, Гейдельберг: Springer. стр. 547–560. дои : 10.1007/978-3-540-73368-3_54 . ISBN 978-3-540-73368-3 .
^ Ньювенхейс, Р.; Оливерас, А.; Тинелли, К. (2006), «Решение теорий SAT и SAT по модулю: от абстрактной процедуры Дэвиса-Патнэма-Логеманна-Лавленда к DPLL (T)» (PDF) , Journal of the ACM , vol. 53, стр. 937–977, doi : 10.1145/1217856.1217859 , S2CID 14058631.
^ де Моура, Леонардо; Бьёрнер, Николай (12–15 августа 2008 г.). «Эффективное решение пропозициональной логики с использованием DPLL и наборов подстановок» . В Армандо, Алессандро; Баумгартнер, Питер; Доук, Жиль (ред.). Автоматизированное рассуждение . 4-я Международная совместная конференция по автоматизированному рассуждению, Сидней, Новый Южный Уэльс, Австралия. Конспекты лекций по информатике. Берлин, Гейдельберг: Springer. стр. 410–425. дои : 10.1007/978-3-540-71070-7_35 . ISBN 978-3-540-71070-7 .
^ Хадарян, Лиана; Бансал, Кшитидж; Йованович, Деян; Барретт, Кларк; Тинелли, Чезаре (2014). «Повесть о двух решателях: нетерпеливые и ленивые подходы к бит-векторам» . В Бьере, Армин; Блум, Родерик (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 8559. Чам: Springer International Publishing. стр. 680–695. дои : 10.1007/978-3-319-08867-9_45 . ISBN 978-3-319-08867-9 .
^ Брэйн, Мартин; Шанда, Флориан; Сунь, Ючэн (2019). «Улучшенная обработка битов для задач с плавающей запятой» . В Войнаре, Томаш; Чжан, Лицзюнь (ред.). Инструменты и алгоритмы построения и анализа систем . 25-я Международная конференция «Инструменты и алгоритмы построения и анализа систем 2019», Прага, Чехия, 6–11 апреля 2019 г., Материалы, Часть I. Конспект лекций по информатике. Чам: Международное издательство Springer. стр. 79–98. дои : 10.1007/978-3-030-17462-0_5 . ISBN 978-3-030-17462-0 . S2CID 92999474 .
^ Брэйн, Мартин; Нимец, Айна; Прейнер, Матиас; Рейнольдс, Эндрю; Барретт, Кларк; Тинелли, Чезаре (2019). «Условия обратимости формул с плавающей запятой» . В Диллиге, Исил; Тасиран, Сердар (ред.). Компьютерная проверка . 31-я Международная конференция «Компьютерная верификация 2019», Нью-Йорк, 15–18 июля 2019 г. Конспекты лекций по информатике. Чам: Международное издательство Springer. стр. 116–136. дои : 10.1007/978-3-030-25543-5_8 . ISBN 978-3-030-25543-5 . S2CID 196613701 .
^ Лян, Тяньи; Цискаридзе, Нестан; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк (2015). «Процедура принятия решения для обычного членства и ограничений длины неограниченных строк» . В Лутце, Карстен; Ранисе, Сильвио (ред.). Границы объединения систем . Конспекты лекций по информатике. Том. 9322. Чам: Springer International Publishing. стр. 135–150. дои : 10.1007/978-3-319-24246-0_9 . ISBN 978-3-319-24246-0 .
^ Рейнольдс, Эндрю; Бланшетт, Жасмин Кристиан (2015). «Процедура принятия решения для (Co) типов данных в решателях SMT» . В Фелти, Эми П.; Мидделдорп, Аарт (ред.). Автоматизированный вычет – CADE-25 . Конспекты лекций по информатике. Том. 9195. Чам: Springer International Publishing. стр. 197–213. дои : 10.1007/978-3-319-21401-6_13 . ISBN 978-3-319-21401-6 .
^ Шэн, Ин; Нётцли, Андрес; Рейнольдс, Эндрю; Зоар, Йони; Дилл, Дэвид; Грискамп, Вольфганг; Парк, Джанкил; Кадир, Шаз; Барретт, Кларк; Тинелли, Чезаре (15 сентября 2023 г.). «Рассуждения о векторах: выполнимость по модулю теории последовательностей» . Журнал автоматизированного рассуждения . 67 (3): 32. дои : 10.1007/s10817-023-09682-2 . ISSN 1573-0670 . S2CID 261829653 .
^ Бансал, Кшитидж; Рейнольдс, Эндрю; Барретт, Кларк; Тинелли, Чезаре (2016). «Новая процедура принятия решений для конечных множеств и ограничений мощности в SMT» . В Оливетти, Никола; Тивари, Ашиш (ред.). Автоматизированное рассуждение . Конспекты лекций по информатике. Том. 9706. Чам: Springer International Publishing. стр. 82–98. дои : 10.1007/978-3-319-40229-1_7 . ISBN 978-3-319-40229-1 .
^ Мэн, Баоло; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк (2017). «Решение реляционных ограничений в SMT» . В де Моура, Леонардо (ред.). Автоматический вычет – CADE 26 . Конспекты лекций по информатике. Том. 10395. Чам: Springer International Publishing. стр. 148–165. дои : 10.1007/978-3-319-63046-5_10 . ISBN 978-3-319-63046-5 .
^ Рейнольдс, Эндрю; Иосиф, Раду; Сербан, Кристина; Кинг, Тим (2016). «Процедура принятия решения для логики разделения в SMT» (PDF) . В Арто, Сирилл; Легай, Аксель; Пелед, Дорон (ред.). Автоматизированная технология проверки и анализа . Конспекты лекций по информатике. Том. 9938. Чам: Springer International Publishing. стр. 244–261. дои : 10.1007/978-3-319-46520-3_16 . ISBN 978-3-319-46520-3 . S2CID 6753369 .
^ Оздемир, Алекс; Кремер, Гереон; Тинелли, Чезаре; Барретт, Кларк (2023). «Выполнимость по модулю конечных полей» . В Энее Константин; Лал, Акаш (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 13965. Чам: Springer Nature Switzerland. стр. 163–186. дои : 10.1007/978-3-031-37703-7_8 . ISBN 978-3-031-37703-7 . S2CID 257235627 .
^ Бэйлесс, Сэм; Бэйлесс, Ной; Хус, Хольгер; Ху, Алан (04 марта 2015 г.). «Монотонные теории SAT по модулю» . Материалы конференции AAAI по искусственному интеллекту . 29 (1). arXiv : 1406.0043 . дои : 10.1609/aaai.v29i1.9755 . ISSN 2374-3468 . S2CID 9567647 .
^ Кленце, Тобиас; Бэйлесс, Сэм; Ху, Алан Дж. (2016). «Быстрый, гибкий и минимальный синтез CTL с помощью SMT» . В Чаудхури, Сварат; Фарзан, Азаде (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 9779. Чам: Springer International Publishing. стр. 136–156. дои : 10.1007/978-3-319-41528-4_8 . ISBN 978-3-319-41528-4 .
^ Бембенек, Аарон; Гринберг, Майкл; Чонг, Стивен (11 января 2023 г.). «От SMT к ASP: подходы к решению задач синтеза журналов данных как выбора правил на основе решателей» . Труды ACM по языкам программирования . 7 (ПОПЛ): 7:185–7:217. дои : 10.1145/3571200 . S2CID 253525805 .
^ Бауэр, А.; Пистер, М.; Таутшниг, М. (2007), «Инструментальная поддержка для анализа гибридных систем и моделей», Труды конференции 2007 года по проектированию, автоматизации и испытаниям в Европе (ДАТА'07) , Компьютерное общество IEEE, стр. 1, CiteSeerX 10.1.1.323.6807 , doi : 10.1109/DATE.2007.364411 , ISBN 978-3-9810801-2-4 , S2CID 9159847
^ Френцле, М.; Херде, К.; Ратчан, С.; Шуберт, Т.; Тейдж, Т. (2007), «Эффективное решение больших нелинейных арифметических систем ограничений со сложной логической структурой» (PDF) , Журнал по выполнимости, логическому моделированию и вычислениям , 1 (3–4 Специальный выпуск JSAT по интеграции SAT/CP ): 209–236, doi : 10.3233/SAT190012
^ Барбоза, Ханиэль; Барретт, Кларк; Брэйн, Мартин; Кремер, Гереон; Лахнитт, Ханна; Манн, Макай; Мохамед, Абдалрахман; Мохамед, Мудатир; Нимец, Айна; Нётцли, Андрес; Оздемир, Алекс; Прейнер, Матиас; Рейнольдс, Эндрю; Шэн, Ин; Тинелли, Чезаре (2022). «cvc5: универсальный и мощный SMT-решатель» . В Фисмане, Дана; Розу, Григоре (ред.). Инструменты и алгоритмы построения и анализа систем, 28-я Международная конференция . Конспекты лекций по информатике. Том. 13243. Чам: Springer International Publishing. стр. 415–442. дои : 10.1007/978-3-030-99524-9_24 . ISBN 978-3-030-99524-9 . S2CID 247857361 .
^ Барретт, Кларк; де Моура, Леонардо; Стамп, Аарон (2005). «SMT-COMP: Конкурс теорий выполнимости по модулю» . В Этессами – Куша; Раджамани, Шрирам К. (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 3576. Спрингер. стр. 20–23. дои : 10.1007/11513988_4 . ISBN 978-3-540-31686-2 .
^ Барретт, Кларк; де Моура, Леонардо; Ранисе, Сильвио; Стамп, Аарон; Тинелли, Чезаре (2011). «Инициатива SMT-LIB и развитие SMT: (обсуждение награды HVC 2010)». В Барнере, Шэрон; Харрис, Ян; Кренинг, Дэниел; Раз, Орна (ред.). Аппаратное и программное обеспечение: проверка и тестирование . Конспекты лекций по информатике. Том. 6504. Спрингер. п. 3. Бибкод : 2011LNCS.6504....3B . дои : 10.1007/978-3-642-19583-9_2 . ISBN 978-3-642-19583-9 .
^ «СМТ-КОМП 2020» . СМТ-КОМП . Проверено 19 октября 2020 г.
^ Хасан, Мостафа; Урбан, Катерина; Эйлерс, Марко; Мюллер, Питер (2018). «Вывод типов на основе MaxSMT для Python 3» . Компьютерная проверка . Конспекты лекций по информатике. Том. 10982. стр. 12–19. дои : 10.1007/978-3-319-96142-2_2 . ISBN 978-3-319-96141-5 .
^ Лонкарик, Кальвин и др. «Практическая основа объяснения ошибок вывода типа». Уведомления ACM SIGPLAN 51.10 (2016 г.): 781–799.
^ Бомонт, Пол; Эванс, Нил; Хут, Майкл; Плант, Том (2015). «Анализ уверенности в контроле над ядерным оружием: абстракции SMT байесовских сетей убеждений». В Пернуле, Гюнтер; Я. Райан, Питер; Вейппль, Эдгар (ред.). Компьютерная безопасность -- ESORICS 2015 . Конспекты лекций по информатике. Том. 9326. Спрингер. стр. 521–540. дои : 10.1007/978-3-319-24174-6_27 . ISBN 978-3-319-24174-6 .
^ Экичи, Бурак; Мебсаут, Ален; Тинелли, Чезаре; Келлер, Шанталь; Кац, Гай; Рейнольдс, Эндрю; Барретт, Кларк (2017). «SMTCoq: плагин для интеграции решателей SMT в Coq» (PDF) . В Маджумдаре — Рупак; Кунчак, Виктор (ред.). Компьютерная верификация, 29-я Международная конференция . Конспекты лекций по информатике. Том. 10427. Чам: Springer International Publishing. стр. 126–133. дои : 10.1007/978-3-319-63390-9_7 . ISBN 978-3-319-63390-9 . S2CID 206701576 .
^ Бланшетт, Жасмин Кристиан; Бёме, Саша; Полсон, Лоуренс К. (01 июня 2013 г.). «Расширение кувалды с помощью решателей SMT» . Журнал автоматизированного рассуждения . 51 (1): 109–128. дои : 10.1007/s10817-013-9278-5 . ISSN 1573-0670 .

Ссылки

Барретт, К.; Себастьяни, Р.; Сешиа, С.; Тинелли, К. (2009). «Теории выполнимости по модулю» . В Бьере, А.; Хойле, MJH; ван Маарен, Х.; Уолш, Т. (ред.). Справочник по выполнимости . Границы искусственного интеллекта и приложений. Том. 185. ИОС Пресс. стр. 825–885. ISBN 9781607503767 .
Ганеш, Виджай (сентябрь 2007 г.). Процедуры принятия решений для битовых векторов, массивов и целых чисел (PDF) (доктор философии). Факультет компьютерных наук Стэнфордского университета.
Джа, Саммит; Лимайе, Ришикеш; Сешиа, Санджит А. (2009). «Бивер: разработка эффективного SMT-решателя для бит-векторной арифметики». Материалы 21-й Международной конференции по компьютерному контролю . стр. 668–674. дои : 10.1007/978-3-642-02658-4_53 . ISBN 978-3-642-02658-4 .
Брайант, RE; немецкий, СМ; Велев, Миннесота (1999). «Верификация микропроцессора с использованием эффективных процедур принятия решений для логики равенства с неинтерпретируемыми функциями» (PDF) . Аналитические таблицы и родственные методы . стр. 1–13. , стр. , .
Дэвис, М.; Патнэм, Х. (1960). «Вычислительная процедура для количественной теории» . Журнал Ассоциации вычислительной техники . 7 (3): 201–215. дои : 10.1145/321033.321034 . S2CID 31888376 .
Дэвис, М.; Логеманн, Г.; Лавленд, Д. (1962). «Машинная программа для доказательства теорем». Коммуникации АКМ . 5 (7): 394–397. дои : 10.1145/368273.368557 . hdl : 2027/mdp.39015095248095 . S2CID 15866917 .
Кренинг, Д.; Стричман, О. (2008). Процедуры принятия решений — алгоритмический взгляд . Серия «Теоретическая информатика». Спрингер. ISBN 978-3-540-74104-6 .
Нам, Г.-Ж.; Сакалла, штат Калифорния; Рутенбар, Р. (2002). «Новый подход к детальной маршрутизации FPGA с помощью логической выполнимости на основе поиска». Транзакции IEEE по автоматизированному проектированию интегральных схем и систем . 21 (6): 674–684. дои : 10.1109/TCAD.2002.1004311 .
SMT-LIB: Библиотека теорий выполнимости по модулю
SMT-COMP: Конкурс теорий выполнимости по модулю
Процедуры принятия решений – алгоритмическая точка зрения
Себастиани, Р. (2007). «Теории ленивой выполнимости по модулю». Журнал по выполнимости, логическому моделированию и вычислениям . 3 (3–4): 141–224. CiteSeerX 10.1.1.100.221 . дои : 10.3233/SAT190034 .

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

[1] Бланшетт, Жасмин Кристиан; Бёме, Саша; Полсон, Лоуренс К. (01 июня 2013 г.). «Расширение кувалды с помощью решателей SMT» . Журнал автоматизированного рассуждения . 51 (1): 109–128. дои : 10.1007/s10817-013-9278-5 . ISSN 1573-0670 . Решатели ATP и SMT имеют взаимодополняющие преимущества. Первые более элегантно справляются с квантификаторами, тогда как вторые превосходно справляются с большими, в основном наземными задачами.

[2] Вебер, Тьярк; Коншон, Сильвен; Дехарб, Давид; Хейцманн, Матиас; Нимец, Айна; Регер, Джайлз (01 января 2019 г.). «Конкурс СМТ 2015–2018» . Журнал по выполнимости, логическому моделированию и вычислениям . 11 (1): 221–259. дои : 10.3233/SAT190123 . S2CID 210147712 . В последние годы мы наблюдаем стирание границ между SMT-COMP и CASC: решатели SMT конкурируют в CASC, а ATP — в SMT-COMP.

[3] Барбоза, Ханиэль; Рейнольдс, Эндрю; Эль Урауи, Дэниел; Тинелли, Чезаре; Барретт, Кларк (2019). «Расширение решателей SMT на логику высшего порядка» . Автоматический дедукция – CADE 27: 27-я Международная конференция по автоматическому дедукции, Натал, Бразилия, 27–30 августа 2019 г., Материалы . Спрингер. стр. 35–54. дои : 10.1007/978-3-030-29436-6_3 . ISBN 978-3-030-29436-6 . S2CID 85443815 . hal-02300986.

[4] Бруттомессо, Роберто; Чиматти, Алессандро; Франзен, Андерс; Гриджио, Альберто; Ханна, Зияд; Надель, Александр; Палти, Амит; Себастьяни, Роберто (2007). «Ленивый и многоуровневый SMT($\mathcal{BV}$) решатель для сложных задач промышленной верификации» . В Дамме, Вернер; Германнс, Хольгер (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 4590. Берлин, Гейдельберг: Springer. стр. 547–560. дои : 10.1007/978-3-540-73368-3_54 . ISBN 978-3-540-73368-3 .

[5] Ньювенхейс, Р.; Оливерас, А.; Тинелли, К. (2006), «Решение теорий SAT и SAT по модулю: от абстрактной процедуры Дэвиса-Патнэма-Логеманна-Лавленда к DPLL (T)» (PDF) , Journal of the ACM , vol. 53, стр. 937–977, doi : 10.1145/1217856.1217859 , S2CID 14058631.

[6] де Моура, Леонардо; Бьёрнер, Николай (12–15 августа 2008 г.). «Эффективное решение пропозициональной логики с использованием DPLL и наборов подстановок» . В Армандо, Алессандро; Баумгартнер, Питер; Доук, Жиль (ред.). Автоматизированное рассуждение . 4-я Международная совместная конференция по автоматизированному рассуждению, Сидней, Новый Южный Уэльс, Австралия. Конспекты лекций по информатике. Берлин, Гейдельберг: Springer. стр. 410–425. дои : 10.1007/978-3-540-71070-7_35 . ISBN 978-3-540-71070-7 .

[7] Хадарян, Лиана; Бансал, Кшитидж; Йованович, Деян; Барретт, Кларк; Тинелли, Чезаре (2014). «Повесть о двух решателях: нетерпеливые и ленивые подходы к бит-векторам» . В Бьере, Армин; Блум, Родерик (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 8559. Чам: Springer International Publishing. стр. 680–695. дои : 10.1007/978-3-319-08867-9_45 . ISBN 978-3-319-08867-9 .

[8] Брэйн, Мартин; Шанда, Флориан; Сунь, Ючэн (2019). «Улучшенная обработка битов для задач с плавающей запятой» . В Войнаре, Томаш; Чжан, Лицзюнь (ред.). Инструменты и алгоритмы построения и анализа систем . 25-я Международная конференция «Инструменты и алгоритмы построения и анализа систем 2019», Прага, Чехия, 6–11 апреля 2019 г., Материалы, Часть I. Конспект лекций по информатике. Чам: Международное издательство Springer. стр. 79–98. дои : 10.1007/978-3-030-17462-0_5 . ISBN 978-3-030-17462-0 . S2CID 92999474 .

[9] Брэйн, Мартин; Нимец, Айна; Прейнер, Матиас; Рейнольдс, Эндрю; Барретт, Кларк; Тинелли, Чезаре (2019). «Условия обратимости формул с плавающей запятой» . В Диллиге, Исил; Тасиран, Сердар (ред.). Компьютерная проверка . 31-я Международная конференция «Компьютерная верификация 2019», Нью-Йорк, 15–18 июля 2019 г. Конспекты лекций по информатике. Чам: Международное издательство Springer. стр. 116–136. дои : 10.1007/978-3-030-25543-5_8 . ISBN 978-3-030-25543-5 . S2CID 196613701 .

[10] Лян, Тяньи; Цискаридзе, Нестан; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк (2015). «Процедура принятия решения для обычного членства и ограничений длины неограниченных строк» . В Лутце, Карстен; Ранисе, Сильвио (ред.). Границы объединения систем . Конспекты лекций по информатике. Том. 9322. Чам: Springer International Publishing. стр. 135–150. дои : 10.1007/978-3-319-24246-0_9 . ISBN 978-3-319-24246-0 .

[11] Рейнольдс, Эндрю; Бланшетт, Жасмин Кристиан (2015). «Процедура принятия решения для (Co) типов данных в решателях SMT» . В Фелти, Эми П.; Мидделдорп, Аарт (ред.). Автоматизированный вычет – CADE-25 . Конспекты лекций по информатике. Том. 9195. Чам: Springer International Publishing. стр. 197–213. дои : 10.1007/978-3-319-21401-6_13 . ISBN 978-3-319-21401-6 .

[12] Шэн, Ин; Нётцли, Андрес; Рейнольдс, Эндрю; Зоар, Йони; Дилл, Дэвид; Грискамп, Вольфганг; Парк, Джанкил; Кадир, Шаз; Барретт, Кларк; Тинелли, Чезаре (15 сентября 2023 г.). «Рассуждения о векторах: выполнимость по модулю теории последовательностей» . Журнал автоматизированного рассуждения . 67 (3): 32. дои : 10.1007/s10817-023-09682-2 . ISSN 1573-0670 . S2CID 261829653 .

[13] Бансал, Кшитидж; Рейнольдс, Эндрю; Барретт, Кларк; Тинелли, Чезаре (2016). «Новая процедура принятия решений для конечных множеств и ограничений мощности в SMT» . В Оливетти, Никола; Тивари, Ашиш (ред.). Автоматизированное рассуждение . Конспекты лекций по информатике. Том. 9706. Чам: Springer International Publishing. стр. 82–98. дои : 10.1007/978-3-319-40229-1_7 . ISBN 978-3-319-40229-1 .

[14] Мэн, Баоло; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк (2017). «Решение реляционных ограничений в SMT» . В де Моура, Леонардо (ред.). Автоматический вычет – CADE 26 . Конспекты лекций по информатике. Том. 10395. Чам: Springer International Publishing. стр. 148–165. дои : 10.1007/978-3-319-63046-5_10 . ISBN 978-3-319-63046-5 .

[15] Рейнольдс, Эндрю; Иосиф, Раду; Сербан, Кристина; Кинг, Тим (2016). «Процедура принятия решения для логики разделения в SMT» (PDF) . В Арто, Сирилл; Легай, Аксель; Пелед, Дорон (ред.). Автоматизированная технология проверки и анализа . Конспекты лекций по информатике. Том. 9938. Чам: Springer International Publishing. стр. 244–261. дои : 10.1007/978-3-319-46520-3_16 . ISBN 978-3-319-46520-3 . S2CID 6753369 .

[16] Оздемир, Алекс; Кремер, Гереон; Тинелли, Чезаре; Барретт, Кларк (2023). «Выполнимость по модулю конечных полей» . В Энее Константин; Лал, Акаш (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 13965. Чам: Springer Nature Switzerland. стр. 163–186. дои : 10.1007/978-3-031-37703-7_8 . ISBN 978-3-031-37703-7 . S2CID 257235627 .

[17] Бэйлесс, Сэм; Бэйлесс, Ной; Хус, Хольгер; Ху, Алан (04 марта 2015 г.). «Монотонные теории SAT по модулю» . Материалы конференции AAAI по искусственному интеллекту . 29 (1). arXiv : 1406.0043 . дои : 10.1609/aaai.v29i1.9755 . ISSN 2374-3468 . S2CID 9567647 .

[18] Кленце, Тобиас; Бэйлесс, Сэм; Ху, Алан Дж. (2016). «Быстрый, гибкий и минимальный синтез CTL с помощью SMT» . В Чаудхури, Сварат; Фарзан, Азаде (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 9779. Чам: Springer International Publishing. стр. 136–156. дои : 10.1007/978-3-319-41528-4_8 . ISBN 978-3-319-41528-4 .

[19] Бембенек, Аарон; Гринберг, Майкл; Чонг, Стивен (11 января 2023 г.). «От SMT к ASP: подходы к решению задач синтеза журналов данных как выбора правил на основе решателей» . Труды ACM по языкам программирования . 7 (ПОПЛ): 7:185–7:217. дои : 10.1145/3571200 . S2CID 253525805 .

[20] Бауэр, А.; Пистер, М.; Таутшниг, М. (2007), «Инструментальная поддержка для анализа гибридных систем и моделей», Труды конференции 2007 года по проектированию, автоматизации и испытаниям в Европе (ДАТА'07) , Компьютерное общество IEEE, стр. 1, CiteSeerX 10.1.1.323.6807 , doi : 10.1109/DATE.2007.364411 , ISBN 978-3-9810801-2-4 , S2CID 9159847

[21] Френцле, М.; Херде, К.; Ратчан, С.; Шуберт, Т.; Тейдж, Т. (2007), «Эффективное решение больших нелинейных арифметических систем ограничений со сложной логической структурой» (PDF) , Журнал по выполнимости, логическому моделированию и вычислениям , 1 (3–4 Специальный выпуск JSAT по интеграции SAT/CP ): 209–236, doi : 10.3233/SAT190012

[22] Барбоза, Ханиэль; Барретт, Кларк; Брэйн, Мартин; Кремер, Гереон; Лахнитт, Ханна; Манн, Макай; Мохамед, Абдалрахман; Мохамед, Мудатир; Нимец, Айна; Нётцли, Андрес; Оздемир, Алекс; Прейнер, Матиас; Рейнольдс, Эндрю; Шэн, Ин; Тинелли, Чезаре (2022). «cvc5: универсальный и мощный SMT-решатель» . В Фисмане, Дана; Розу, Григоре (ред.). Инструменты и алгоритмы построения и анализа систем, 28-я Международная конференция . Конспекты лекций по информатике. Том. 13243. Чам: Springer International Publishing. стр. 415–442. дои : 10.1007/978-3-030-99524-9_24 . ISBN 978-3-030-99524-9 . S2CID 247857361 .

[23] Барретт, Кларк; де Моура, Леонардо; Стамп, Аарон (2005). «SMT-COMP: Конкурс теорий выполнимости по модулю» . В Этессами – Куша; Раджамани, Шрирам К. (ред.). Компьютерная проверка . Конспекты лекций по информатике. Том. 3576. Спрингер. стр. 20–23. дои : 10.1007/11513988_4 . ISBN 978-3-540-31686-2 .

[24] Барретт, Кларк; де Моура, Леонардо; Ранисе, Сильвио; Стамп, Аарон; Тинелли, Чезаре (2011). «Инициатива SMT-LIB и развитие SMT: (обсуждение награды HVC 2010)». В Барнере, Шэрон; Харрис, Ян; Кренинг, Дэниел; Раз, Орна (ред.). Аппаратное и программное обеспечение: проверка и тестирование . Конспекты лекций по информатике. Том. 6504. Спрингер. п. 3. Бибкод : 2011LNCS.6504....3B . дои : 10.1007/978-3-642-19583-9_2 . ISBN 978-3-642-19583-9 .

[25] «СМТ-КОМП 2020» . СМТ-КОМП . Проверено 19 октября 2020 г.

[26] Хасан, Мостафа; Урбан, Катерина; Эйлерс, Марко; Мюллер, Питер (2018). «Вывод типов на основе MaxSMT для Python 3» . Компьютерная проверка . Конспекты лекций по информатике. Том. 10982. стр. 12–19. дои : 10.1007/978-3-319-96142-2_2 . ISBN 978-3-319-96141-5 .

[27] Лонкарик, Кальвин и др. «Практическая основа объяснения ошибок вывода типа». Уведомления ACM SIGPLAN 51.10 (2016 г.): 781–799.

[28] Бомонт, Пол; Эванс, Нил; Хут, Майкл; Плант, Том (2015). «Анализ уверенности в контроле над ядерным оружием: абстракции SMT байесовских сетей убеждений». В Пернуле, Гюнтер; Я. Райан, Питер; Вейппль, Эдгар (ред.). Компьютерная безопасность -- ESORICS 2015 . Конспекты лекций по информатике. Том. 9326. Спрингер. стр. 521–540. дои : 10.1007/978-3-319-24174-6_27 . ISBN 978-3-319-24174-6 .

[29] Экичи, Бурак; Мебсаут, Ален; Тинелли, Чезаре; Келлер, Шанталь; Кац, Гай; Рейнольдс, Эндрю; Барретт, Кларк (2017). «SMTCoq: плагин для интеграции решателей SMT в Coq» (PDF) . В Маджумдаре — Рупак; Кунчак, Виктор (ред.). Компьютерная верификация, 29-я Международная конференция . Конспекты лекций по информатике. Том. 10427. Чам: Springer International Publishing. стр. 126–133. дои : 10.1007/978-3-319-63390-9_7 . ISBN 978-3-319-63390-9 . S2CID 206701576 .

[30] Бланшетт, Жасмин Кристиан; Бёме, Саша; Полсон, Лоуренс К. (01 июня 2013 г.). «Расширение кувалды с помощью решателей SMT» . Журнал автоматизированного рассуждения . 51 (1): 109–128. дои : 10.1007/s10817-013-9278-5 . ISSN 1573-0670 .

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

[29]

[30]