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

Логическая задача, изучаемая в информатике

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

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

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

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

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

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

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

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

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

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

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

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

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

Подходы к решению

Ранние попытки решения экземпляров SMT включали их перевод в экземпляры Boolean SAT (например, 32-битная целочисленная переменная кодировалась 32 однобитными переменными с соответствующими весами, а операции на уровне слов, такие как «плюс», заменялись логическими операциями более низкого уровня над битами) и передачу этой формулы в решатель Boolean SAT. Этот подход, который называется жадным подходом (или bitblasting ), имеет свои достоинства: путем предварительной обработки формулы SMT в эквивалентную формулу Boolean SAT существующие решатели Boolean SAT можно использовать «как есть» , а их производительность и производительность улучшаются с течением времени. С другой стороны, потеря высокоуровневой семантики базовых теорий означает, что булевский решатель SAT должен работать намного усерднее, чем необходимо, чтобы обнаружить «очевидные» факты (например, для сложения целых чисел). Это наблюдение привело к разработке ряда решателей SMT, которые тесно интегрируют булевские рассуждения поиска в стиле DPLL с решателями, специфичными для теории ( T-решателями ), которые обрабатывают конъюнкции (AND) предикатов из заданной теории. Этот подход называется ленивым подходом . ^[4] ${\displaystyle 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 подчиняются аксиоме

${\displaystyle 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 на нелинейные теории, такие как определение того, является ли следующее уравнение выполнимым:

${\displaystyle {\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}}}$

где

${\displaystyle 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 .

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

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

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

Формат SMT-LIB также поставляется с рядом стандартизированных тестов и позволил проводить ежегодные соревнования между решателями SMT под названием SMT-COMP. Первоначально соревнование проводилось во время конференции Computer Aided Verification (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; 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);
• Rodin , фреймворк B-метода, разработанный Systerel, может использовать Alt-Ergo в качестве бэкэнда;
• Cubicle — программа проверки моделей с открытым исходным кодом для проверки свойств безопасности систем перехода на основе массивов.
• EasyCrypt — набор инструментов для рассуждений об реляционных свойствах вероятностных вычислений с использованием состязательного кода.

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

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

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

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

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

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

• Программирование набора ответов
• Автоматизированное доказательство теорем
• SAT-решатель
• Логика первого порядка
• Теория чистого равенства

Примечания

1. Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. (2013-06-01). "Extending Sledgehammer with SMT Solvers". Journal of Automated Reasoning . 51 (1): 109–128. doi :10.1007/s10817-013-9278-5. ISSN  1573-0670. ATP и SMT Solvers имеют взаимодополняющие сильные стороны. Первые справляются с квантификаторами более элегантно, тогда как вторые преуспевают в больших, в основном наземных задачах.
2. Вебер, Тьярк; Коншон, Сильвен; Дехарб, Дэвид; Хайцманн, Маттиас; Нимец, Айна; Регер, Джайлс (01.01.2019). «Конкурс SMT 2015–2018». Журнал по выполнимости, булевому моделированию и вычислениям . 11 (1): 221–259. doi : 10.3233/SAT190123 . S2CID  210147712. В последние годы мы наблюдаем размывание границ между SMT-COMP и CASC, когда решатели SMT конкурируют в CASC, а ATP — в SMT-COMP.
3. Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark (2019). «Расширение решателей SMT до логики более высокого порядка». Автоматизированная дедукция – CADE 27: 27-я Международная конференция по автоматизированной дедукции, Натал, Бразилия, 27–30 августа 2019 г., Труды . Springer. стр. 35–54. doi :10.1007/978-3-030-29436-6_3. ISBN 978-3-030-29436-6. S2CID  85443815. hal-02300986.
4. Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Hanna, Ziyad; Nadel, Alexander; Palti, Amit; Sebastiani, Roberto (2007). "A Lazy and Layered SMT( $\mathcal{BV}$ ) Solver for Hard Industrial Verification Problems". В Damm, Werner; Hermanns, Holger (ред.). Computer Aided Verification . Lecture Notes in Computer Science. Vol. 4590. Berlin, Heidelberg: Springer. pp. 547–560. doi :10.1007/978-3-540-73368-3_54. ISBN 978-3-540-73368-3.
5. Nieuwenhuis, R.; Oliveras, A.; Tinelli, C. (2006), «Решение SAT и теорий SAT по модулю: от абстрактной процедуры Дэвиса-Патнэма-Логемана-Лавленда к DPLL(T)» (PDF) , Журнал ACM , т. 53, стр. 937–977, doi :10.1145/1217856.1217859, S2CID  14058631
6. де Моура, Леонардо; Бьёрнер, Николай (12–15 августа 2008 г.). «Эффективное решение пропозициональной логики с использованием DPLL и множеств подстановки». В Armando, Alessandro; Baumgartner, Peter; Dowek, Gilles (ред.). Автоматизированное рассуждение . 4-я Международная совместная конференция по автоматизированному рассуждению, Сидней, Новый Южный Уэльс, Австралия. Конспект лекций по информатике. Берлин, Гейдельберг: Springer. стр. 410–425. doi :10.1007/978-3-540-71070-7_35. ISBN 978-3-540-71070-7.
7. Хадареан, Лиана; Бансал, Кшитий; Йованович, Деян; Барретт, Кларк; Тинелли, Чезаре (2014). «История двух решателей: энергичные и ленивые подходы к бит-векторам». В Бире, Армин; Блюм, Родерик (ред.). Компьютерная верификация . Конспект лекций по информатике. Том 8559. Cham: Springer International Publishing. стр. 680–695. doi :10.1007/978-3-319-08867-9_45. ISBN 978-3-319-08867-9.
8. Brain, Martin; Schanda, Florian; Sun, Youcheng (2019). «Building Better Bit-Blasting for Floating-Point Problems». В Vojnar, Tomáš; Zhang, Lijun (ред.). Tools and Algorithms for the Construction and Analysis of Systems . 25-я международная конференция, Tools and Algorithms for the Construction and Analysis of Systems 2019, Прага, Чешская Республика, 6–11 апреля 2019 г., Труды, часть I. Конспект лекций по информатике. Cham: Springer International Publishing. стр. 79–98. doi : 10.1007/978-3-030-17462-0_5 . ISBN 978-3-030-17462-0. S2CID  92999474.
9. Brain, Martin; Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2019). «Условия обратимости формул с плавающей точкой». В Dillig, Isil; Tasiran, Serdar (ред.). Computer Aided Verification . 31-я международная конференция Computer Aided Verification 2019, Нью-Йорк, 15–18 июля 2019 г. Lecture Notes in Computer Science. Cham: Springer International Publishing. стр. 116–136. doi : 10.1007/978-3-030-25543-5_8 . ISBN 978-3-030-25543-5. S2CID  196613701.
10. Лян, Тяньи; Цискаридзе, Нестан; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк (2015). «Процедура принятия решений для регулярного членства и ограничений длины для неограниченных строк». В Lutz, Carsten; Ranise, Silvio (ред.). Frontiers of Combining Systems . Lecture Notes in Computer Science. Vol. 9322. Cham: Springer International Publishing. pp. 135–150. doi :10.1007/978-3-319-24246-0_9. ISBN 978-3-319-24246-0.
11. Рейнольдс, Эндрю; Бланшетт, Жасмин Кристиан (2015). «Процедура принятия решения для (Co)типов данных в SMT-решателях». В Felty, Эми П.; Миддельдорп, Аарт (ред.). Автоматизированная дедукция — CADE-25 . Конспект лекций по информатике. Том 9195. Cham: Springer International Publishing. стр. 197–213. doi :10.1007/978-3-319-21401-6_13. ISBN 978-3-319-21401-6.
12. Шэн, Ин; Нётцли, Андрес; Рейнольдс, Эндрю; Зохар, Йони; Дилл, Дэвид; Грискамп, Вольфганг; Парк, Юнкил; Кадир, Шаз; Барретт, Кларк; Тинелли, Чезаре (15.09.2023). «Рассуждения о векторах: выполнимость по модулю теории последовательностей». Журнал автоматизированного рассуждения . 67 (3): 32. doi :10.1007/s10817-023-09682-2. ISSN  1573-0670. S2CID  261829653.
13. Бансал, Кшитидж; Рейнольдс, Эндрю; Барретт, Кларк; Тинелли, Чезаре (2016). «Новая процедура принятия решений для конечных множеств и ограничений мощности в SMT». В Olivetti, Nicola; Tiwari, Ashish (ред.). Автоматизированное рассуждение . Конспект лекций по информатике. Том 9706. Cham: Springer International Publishing. стр. 82–98. doi :10.1007/978-3-319-40229-1_7. ISBN 978-3-319-40229-1.
14. Мэн, Баолуо; Рейнольдс, Эндрю; Тинелли, Чезаре; Барретт, Кларк (2017). «Решение реляционных ограничений в SMT». Ин де Моура, Леонардо (ред.). Автоматизированная дедукция – CADE 26. Конспект лекций по информатике. Том 10395. Cham: Springer International Publishing. стр. 148–165. doi :10.1007/978-3-319-63046-5_10. ISBN 978-3-319-63046-5.
15. Рейнольдс, Эндрю; Иосиф, Раду; Сербан, Кристина; Кинг, Тим (2016). «Процедура принятия решений для логики разделения в SMT» (PDF) . В Artho, Сирилл; Легай, Аксель; Пелед, Дорон (ред.). Автоматизированная технология проверки и анализа . Конспект лекций по информатике. Том 9938. Cham: Springer International Publishing. стр. 244–261. doi : 10.1007/978-3-319-46520-3_16. ISBN 978-3-319-46520-3. S2CID  6753369.
16. Оздемир, Алекс; Кремер, Гереон; Тинелли, Чезаре; Барретт, Кларк (2023). «Выполнимость по модулю конечных полей». В Энеа, Константин; Лал, Акаш (ред.). Компьютерная верификация . Конспект лекций по информатике. Том 13965. Cham: Springer Nature Switzerland. стр. 163–186. doi :10.1007/978-3-031-37703-7_8. ISBN 978-3-031-37703-7. S2CID  257235627.
17. Бейлесс, Сэм; Бейлесс, Ноа; Хус, Хольгер; Ху, Алан (2015-03-04). "SAT Modulo Monotonic Theories". Труды конференции AAAI по искусственному интеллекту . 29 (1). arXiv : 1406.0043 . doi : 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.01.2023). «От SMT к ASP: подходы на основе решателей к решению задач синтеза журналов данных как выбора правил». Труды ACM по языкам программирования . 7 (POPL): 7:185–7:217. doi : 10.1145/3571200 . S2CID  253525805.
20. Бауэр, А.; Пистер, М.; Таушниг, М. (2007), "Инструментальная поддержка для анализа гибридных систем и моделей", Труды конференции 2007 года по проектированию, автоматизации и тестированию в Европе (ДАТА'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
21. Fränzle, M.; Herde, C.; Ratschan, S.; Schubert, T.; Teige, T. (2007), "Эффективное решение больших нелинейных арифметических систем ограничений со сложной булевой структурой" (PDF) , Журнал по выполнимости, булевому моделированию и вычислениям , 1 (3–4 JSAT Специальный выпуск по интеграции SAT/CP): 209–236, doi :10.3233/SAT190012
22. Barbosa, Haniel; Barrett, Clark; Brain, Martin; Kremer, Gereon; Lachnitt, Hanna; Mann, Makai; Mohamed, Abdalrhman; Mohamed, Mudathir; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Reynolds, Andrew; Sheng, Ying; Tinelli, Cesare (2022). "cvc5: универсальный и промышленный решатель SMT". В Fisman, Dana; Rosu, Grigore (ред.). Инструменты и алгоритмы для построения и анализа систем, 28-я международная конференция . Конспект лекций по информатике. Том 13243. Cham: 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. Springer. С. 20–23. doi :10.1007/11513988_4. ISBN 978-3-540-31686-2.
24. Барретт, Кларк; де Моура, Леонардо; Ранис, Сильвио; Стамп, Аарон; Тинелли, Чезаре (2011). «Инициатива SMT-LIB и рост SMT: (HVC 2010 Award Talk)». В Барнер, Шарон; Харрис, Ян; Кренинг, Дэниел; Раз, Орна (ред.). Аппаратное и программное обеспечение: проверка и тестирование . Конспект лекций по информатике. Том 6504. Springer. стр. 3. Bibcode : 2011LNCS.6504....3B. doi : 10.1007/978-3-642-19583-9_2 . ISBN 978-3-642-19583-9.
25. "SMT-COMP 2020". SMT-COMP . Получено 2020-10-19 .
26. Хассан, Мостафа; Урбан, Катерина; Эйлерс, Марко; Мюллер, Питер (2018). «MaxSMT-Based Type Inference for Python 3». Computer Aided Verification . Lecture Notes in Computer Science. Vol. 10982. pp. 12–19. doi :10.1007/978-3-319-96142-2_2. ISBN 978-3-319-96141-5.
27. Loncaric, Calvin и др. «Практическая структура для объяснения ошибок вывода типов». ACM SIGPLAN Notices 51.10 (2016): 781-799.
28. Бомонт, Пол; Эванс, Нил; Хут, Майкл; Плант, Том (2015). «Анализ уверенности для контроля над ядерным оружием: абстракции SMT байесовских сетей убеждений». В Pernul, Гюнтер; YA Райан, Питер; Вайпль, Эдгар (ред.). Компьютерная безопасность — ESORICS 2015. Конспект лекций по информатике. Том 9326. Springer. С. 521–540. doi : 10.1007/978-3-319-24174-6_27 . ISBN 978-3-319-24174-6.
29. Экичи, Бурак; Мебсоут, Ален; Тинелли, Чезаре; Келлер, Шанталь; Кац, Гай; Рейнольдс, Эндрю; Барретт, Кларк (2017). "SMTCoq: плагин для интеграции SMT-решателей в Coq" (PDF) . В Маджумдар, Рупак; Кунчак, Виктор (ред.). Computer Aided Verification, 29th International Conference . Lecture Notes in Computer Science. Vol. 10427. Cham: Springer International Publishing. pp. 126–133. doi :10.1007/978-3-319-63390-9_7. ISBN 978-3-319-63390-9. S2CID  206701576.
30. Бланшетт, Жасмин Кристиан; Бёме, Саша; Полсон, Лоуренс К. (2013-06-01). «Расширение Sledgehammer с помощью SMT Solvers». Журнал автоматизированного рассуждения . 51 (1): 109–128. doi :10.1007/s10817-013-9278-5. ISSN  1573-0670.

Ссылки

• Barrett, C.; Sebastiani, R.; Seshia, S.; Tinelli, C. (2009). «Выполнимость по модулю теорий». В Biere, A.; Heule, MJH; van Maaren, H.; Walsh, T. (ред.). Справочник по выполнимости . Границы искусственного интеллекта и приложений. Том 185. IOS Press. С. 825–885. ISBN 9781607503767.
• Ганеш, Виджай (сентябрь 2007 г.). Процедуры принятия решений для битовых векторов, массивов и целых чисел (PDF) (PhD). Кафедра компьютерных наук, Стэнфордский университет.
• Jha, Susmit; Limaye, Rhishikesh; Seshia, Sanjit A. (2009). "Beaver: Engineering an efficient SMT Solver for bit-vector arithmetic". Труды 21-й Международной конференции по компьютерной верификации . С. 668–674. doi :10.1007/978-3-642-02658-4_53. ISBN 978-3-642-02658-4.
• Брайант, Р. Э.; Герман, С. М.; Велев, М. Н. (1999). «Проверка микропроцессора с использованием эффективных процедур принятия решений для логики равенства с неинтерпретируемыми функциями» (PDF) . Аналитические таблицы и связанные с ними методы . стр. 1–13., стр. , .
• Дэвис, М.; Патнэм, Х. (1960). «Вычислительная процедура для квантификационной теории». Журнал Ассоциации вычислительной техники . 7 (3): 201–215. doi : 10.1145/321033.321034 . S2CID  31888376.
• Дэвис, М.; Логеманн, Г.; Лавленд, Д. (1962). «Машинная программа для доказательства теорем». Сообщения ACM . 5 (7): 394–397. doi :10.1145/368273.368557. hdl : 2027/mdp.39015095248095 . S2CID  15866917.
• Kroening, D.; Strichman, O. (2008). Процедуры принятия решений — алгоритмическая точка зрения. Серия Theoretical Computer Science. Springer. ISBN 978-3-540-74104-6.
• Нам, Г.-Дж.; Сакаллах, КА; Рутенбар, Р. (2002). «Новый подход к подробной маршрутизации ПЛИС с использованием выполнимости булевых выражений на основе поиска». Труды IEEE по автоматизированному проектированию интегральных схем и систем . 21 (6): 674–684. doi :10.1109/TCAD.2002.1004311.
• SMT-LIB: Библиотека теорий выполнимости по модулю
• SMT-COMP: Конкурс теорий выполнимости по модулю
• Процедуры принятия решений - алгоритмическая точка зрения
• Себастьяни, Р. (2007). «Ленивые теории выполнимости по модулю». Журнал выполнимости, булевого моделирования и вычислений . 3 (3–4): 141–224. CiteSeerX  10.1.1.100.221 . doi :10.3233/SAT190034.

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