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

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

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

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

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

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

Выполнимость: Определите, является ли выполнимым. $x\vee (y\wedge \neg z)$
Доступ к массиву: найдите значение для массива A такое, что A[0]=5.
Арифметика бит-векторов: определите, являются ли x и y разными 3-битными числами.
Неинтерпретируемые функции: Найдите значения x и y такие, что и . ${\ displaystyle 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 приходится работать намного усерднее, чем необходимо, чтобы обнаружить «очевидные» факты (например, для сложения целых чисел). Это наблюдение привело к разработка ряда решателей SMT, которые тесно интегрируют логические рассуждения поиска в стиле DPLL с решателями, специфичными для теории ( T-солверами ), которые обрабатывают соединения (И) предикатов из данной теории. Этот подход называется ленивым подходом . ^[4] $x+y=y+x$

Эта архитектура , получившая название 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)\подразумевает 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.3 y)\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, основанный на унификации решения SAT DPLL и распространения интервальных ограничений , называемой алгоритмом iSAT ^[21] и cvc5 . ^[22]

Решатели

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

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

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

Существует множество попыток описать стандартизированный интерфейс для решателей SMT (и автоматизированных средств доказательства теорем — термин, часто используемый как синоним). Наиболее известным является стандарт SMT-LIB, ^{[ нужна ссылка ]} , который предоставляет язык, основанный на S-выражениях . Другими ^обычно поддерживаемыми стандартизированными форматами являются формат DIMACS, ^{поддерживаемый} многими решателями логических 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] и Isabelle/HOL . ^[30]

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

Примечания

^ Бланшетт, Жасмин Кристиан; Бёме, Саша; Полсон, Лоуренс К. (01 июня 2013 г.). «Расширение Sledgehammer с помощью SMT Solvers». Журнал автоматизированного рассуждения . 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, номер документа : 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 , номер документа : 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 г.). «Расширение Sledgehammer с помощью SMT Solvers». Журнал автоматизированного рассуждения . 51 (1): 109–128. дои : 10.1007/s10817-013-9278-5. ISSN 1573-0670.