В информатике и математической логике , то выполнимость по модулю теория ( SMT ) проблема является проблемой решения для логических формул относительно комбинаций фоновых теорий , выраженных в классической логике первого порядка с равенством. Примерами теорий, обычно используемых в информатике, являются теория действительных чисел , теория целых чисел и теории различных структур данных, таких как списки , массивы , битовые векторы и т. Д. SMT можно рассматривать как формупроблема удовлетворения ограничений и, следовательно, некий формализованный подход к программированию ограничений .
Основная терминология
Формально говоря, экземпляр SMT - это формула в логике первого порядка , где некоторые функции и символы предиката имеют дополнительные интерпретации, а SMT - это проблема определения выполнимости такой формулы. Другими словами, представьте себе пример проблемы логической выполнимости (SAT), в которой некоторые из двоичных переменных заменяются предикатами для подходящего набора небинарных переменных. Предикат - это двоичная функция недвоичных переменных. Примеры предикатов включают линейные неравенства (например,) или равенства, включающие неинтерпретированные термины и функциональные символы (например, где некоторая неопределенная функция двух аргументов). Эти предикаты классифицируются согласно каждой присвоенной теории. Например, линейные неравенства над действительными переменными оцениваются с использованием правил теории линейной вещественной арифметики , тогда как предикаты, включающие неинтерпретированные термины и функциональные символы, оцениваются с использованием правил теории неинтерпретируемых функций с равенством (иногда называемой пустой теорией ). Другие теории включают теории массивов и структур списков (полезные для моделирования и проверки компьютерных программ ) и теорию битовых векторов (полезные при моделировании и проверке конструкции оборудования ). Также возможны подтеории: например, разностная логика - это подтеория линейной арифметики, в которой каждое неравенство ограничивается формой для переменных а также и постоянный .
Большинство решателей SMT поддерживают только бескванторные фрагменты своей логики.
Выразительная сила
Экземпляр SMT - это обобщение логического экземпляра SAT, в котором различные наборы переменных заменяются предикатами из множества лежащих в основе теорий. Формулы SMT предоставляют гораздо более богатый язык моделирования, чем это возможно с булевыми формулами SAT. Например, формула SMT позволяет нам моделировать операции канала данных микропроцессора на уровне слова, а не на уровне битов.
Для сравнения, программирование набора ответов также основано на предикатах (точнее, на атомарных предложениях, созданных из атомарной формулы ). В отличие от SMT, программы с набором ответов не имеют кванторов и не могут легко выразить ограничения, такие как линейная арифметика или разностная логика - ASP в лучшем случае подходит для логических задач, которые сводятся к свободной теории неинтерпретируемых функций. Реализация 32-битных целых чисел в качестве битовых векторов в ASP страдает от большинства проблем, с которыми сталкивались ранние решатели SMT: «очевидные» идентичности, такие как x + y = y + x , трудно вывести.
Программирование с логикой ограничений действительно обеспечивает поддержку линейных арифметических ограничений, но в совершенно другой теоретической структуре. [ необходима цитата ] Решатели SMT также были расширены для решения формул в логике более высокого порядка . [1]
Подходы решателя
Ранние попытки решения экземпляров SMT включали преобразование их в логические экземпляры SAT (например, 32-битная целочисленная переменная будет кодироваться 32 однобитными переменными с соответствующими весами, а операции на уровне слова, такие как `` плюс '', будут заменены на более низкие - логические операции уровня над битами) и передать эту формулу логическому вычислителю SAT. Этот подход, который упоминается как в нетерпеливом подходе , имеет свои преимущество: путь предварительной обработку SMT формулы в эквивалентную булевой SAT существующей Логического SAT решатель можно использовать «как есть» , и их улучшение производительности и емкости заемных средств с течением времени формулы . С другой стороны, потеря высокоуровневой семантики лежащих в основе теорий означает, что логическая программа расчета SAT должна работать намного усерднее, чем это необходимо, для обнаружения «очевидных» фактов (таких какдля сложения целых чисел.) Это наблюдение привело к разработке ряда решателей SMT, которые тесно интегрируют логические рассуждения о поиске в стиле DPLL с решателями, специфичными для теории ( T-решатели ), которые обрабатывают конъюнкции (И) предикатов из заданного теория. Такой подход называется в ленивом подходе .
Дублированный DPLL (Т) , [2] эта архитектура дает ответственность булевых рассуждений на основе DPLL SAT решатель , который, в свою очередь, взаимодействует с решателем для теории T через хорошо определенный интерфейс. Решателю теории нужно беспокоиться только о проверке выполнимости конъюнкций предикатов теории, переданных ему из решателя SAT, когда он исследует булево пространство поиска формулы. Однако для того, чтобы эта интеграция работала хорошо, решатель теории должен иметь возможность участвовать в распространении и анализе конфликтов, т. Е. Он должен иметь возможность выводить новые факты из уже установленных фактов, а также давать краткие объяснения невозможности, когда теория противоречит возникают. Другими словами, решатель теории должен быть инкрементным и иметь возможность обратного отслеживания .
SMT для неразрешимых теорий
Большинство общих подходов к SMT поддерживают разрешимые теории. Однако многие системы реального мира можно смоделировать только с помощью нелинейной арифметики над действительными числами, включая трансцендентные функции , например самолет и его поведение. Этот факт побуждает распространить проблему SMT на нелинейные теории, например, определить, следует ли
где
выполнимо. Тогда такие проблемы вообще становятся неразрешимыми . (Теория вещественных замкнутых полей и, следовательно, полная теория действительных чисел первого порядка , однако, разрешимы с использованием исключения кванторов . Это сделано Альфредом Тарским .) Теория натуральных чисел первого порядка со сложением (но не умножением) , называемая арифметикой Пресбургера , также разрешима. Поскольку умножение на константы может быть реализовано как вложенное сложение, арифметика во многих компьютерных программах может быть выражена с помощью арифметики Пресбургера, что приводит к разрешимым формулам.
Примерами решателей SMT, обращающимися к булевым комбинациям атомов теории из неразрешимых арифметических теорий над действительными числами, являются ABsolver [3], в котором используется классическая архитектура DPLL (T) с пакетом нелинейной оптимизации в качестве (обязательно неполного) решателя теории подчиненных функций, и iSAT , основанный на объединении DPLL SAT-решения и распространения интервальных ограничений, называемый алгоритмом iSAT. [4]
Решатели
В таблице ниже приведены некоторые функции многих доступных решателей SMT. Столбец «SMT-LIB» указывает совместимость с языком SMT-LIB; многие системы, отмеченные «да», могут поддерживать только старые версии SMT-LIB или предлагать только частичную поддержку языка. Столбец «CVC» указывает на поддержку языка CVC. Столбец «DIMACS» указывает на поддержку формата DIMACS .
Проекты различаются не только функциями и производительностью, но и жизнеспособностью окружающего сообщества, его постоянным интересом к проекту и его способностью вносить документацию, исправления, тесты и улучшения.
Платформа | Функции | Заметки | |||||||
---|---|---|---|---|---|---|---|---|---|
Имя | Операционные системы | Лицензия | SMT-LIB | CVC | DIMACS | Встроенные теории | API | SMT-COMP [1] | |
ABsolver | Linux | CPL | v1.2 | Нет | да | линейная арифметика, нелинейная арифметика | C ++ | нет | На основе DPLL |
Альт-Эрго | Linux , Mac OS , Windows | CeCILL-C (примерно эквивалент LGPL ) | частичные v1.2 и v2.0 | Нет | Нет | пустая теория , линейное целое и рациональный арифметик, нелинейные арифметический, полиморфные массивы , перечисленные типов данных , символы переменного тока , битвекторы , запись типов данных , кванторы | OCaml | 2008 г. | Полиморфный язык ввода первого порядка а-ля ML, основанный на SAT-решателе, объединяет подходы типа Шостака и Нельсона-Оппена для рассуждения теорий по модулю |
Barcelogic | Linux | Проприетарный | v1.2 | пустая теория , логика различия | C ++ | 2009 г. | Закрытие конгруэнтности на основе DPLL | ||
Бобр | Linux , Windows | BSD | v1.2 | Нет | Нет | битвекторы | OCaml | 2009 г. | На основе SAT-решателя |
Булектор | Linux | Массачусетский технологический институт | v1.2 | Нет | Нет | битовые векторы , массивы | C | 2009 г. | На основе SAT-решателя |
CVC3 | Linux | BSD | v1.2 | да | пустая теория , линейная арифметика, массивы, кортежи, типы, записи, битовые векторы, кванторы | C / C ++ | 2010 г. | вывод доказательства в HOL | |
CVC4 | Linux , Mac OS , Windows , FreeBSD | BSD | да | да | рациональная и целочисленная линейная арифметика, массивы, кортежи, записи, индуктивные типы данных, битовые векторы, строки и равенство над неинтерпретируемыми функциональными символами | C ++ | 2010 г. | версия 1.5 выпущена в июле 2017 г. | |
Инструментарий процедуры принятия решений (DPT) | Linux | Apache | Нет | OCaml | нет | На основе DPLL | |||
Я сидел | Linux | Проприетарный | Нет | нелинейная арифметика | нет | На основе DPLL | |||
MathSAT | Linux , Mac OS , Windows | Проприетарный | да | да | пустая теория , линейная арифметика, нелинейная арифметика, битовые векторы, массивы | C / C ++ , Python , Java | 2010 г. | На основе DPLL | |
MiniSmt | Linux | LGPL | частичная v2.0 | нелинейная арифметика | 2010 г. | На основе SAT-решателя, на основе Yices | |||
Норн | Решатель SMT для строковых ограничений | ||||||||
OpenCog | Linux | AGPL | Нет | Нет | Нет | вероятностная логика , арифметика. реляционные модели | C ++ , Схема , Python | нет | изоморфизм подграфов |
OpenSMT | Linux , Mac OS , Windows | GPLv3 | частичная v2.0 | да | пустая теория , разности, линейная арифметика, битовые векторы | C ++ | 2011 г. | ленивый SMT Solver | |
расат | Linux | GPLv3 | v2.0 | действительная и целочисленная нелинейная арифметика | 2014, 2015 | Расширение распространения интервальных ограничений с помощью тестирования и теоремы о промежуточном значении | |||
Сатин | ? | Проприетарный | v1.2 | линейная арифметика, разностная логика | никто | 2009 г. | |||
СМТИнтерпол | Linux , Mac OS , Windows | LGPLv3 | v2.5 | неинтерпретируемые функции, линейная вещественная арифметика и линейная целочисленная арифметика | Ява | 2012 г. | Ориентирован на создание высококачественных компактных интерполянтов. | ||
СМЧР | Linux , Mac OS , Windows | GPLv3 | Нет | Нет | Нет | линейная арифметика, нелинейная арифметика, кучи | C | нет | Может реализовывать новые теории с помощью правил обработки ограничений . |
SMT-RAT | Linux , Mac OS | Массачусетский технологический институт | v2.0 | Нет | Нет | линейная арифметика, нелинейная арифметика | C ++ | 2015 г. | Набор инструментов для стратегического и параллельного решения SMT, состоящий из набора совместимых с SMT реализаций. |
SONOLAR | Linux , Windows | Проприетарный | частичная v2.0 | битвекторы | C | 2010 г. | На основе SAT-решателя | ||
Копье | Linux , Mac OS , Windows | Проприетарный | v1.2 | битвекторы | 2008 г. | ||||
STP | Linux , OpenBSD , Windows , Mac OS | Массачусетский технологический институт | частичная v2.0 | да | Нет | битовые векторы, массивы | C , C ++ , Python , OCaml , Java | 2011 г. | На основе SAT-решателя |
МЕЧ | Linux | Проприетарный | v1.2 | битвекторы | 2009 г. | ||||
UCLID | Linux | BSD | Нет | Нет | Нет | пустая теория , линейная арифметика, битовые векторы и ограниченная лямбда (массивы, память, кеш и т. д.) | нет | На основе SAT-решателя, написанного на Московском ML . Язык ввода - проверка модели SMV. Хорошо задокументированы! | |
верит | Linux , OS X | BSD | частичная v2.0 | пустая теория , рациональная и целочисленная линейная арифметика, кванторы и равенство по неинтерпретированным функциональным символам | C / C ++ | 2010 г. | На основе SAT-решателя | ||
Yices | Linux , Mac OS , Windows , FreeBSD | GPLv3 | v2.0 | Нет | да | рациональная и целочисленная линейная арифметика, битовые векторы, массивы и равенство по неинтерпретированным функциональным символам | C | 2014 г. | Исходный код доступен онлайн |
Z3 Доказательство теорем | Linux , Mac OS , Windows , FreeBSD | Массачусетский технологический институт | v2.0 | да | пустая теория , линейная арифметика, нелинейная арифметика, битовые векторы, массивы, типы данных, кванторы , строки | C / C ++ , .NET , OCaml , Python , Java , Haskell | 2011 г. | Исходный код доступен онлайн |
Стандартизация и соревнование решателей SMT-COMP
Есть несколько попыток описать стандартизованный интерфейс для решателей SMT (и автоматических средств доказательства теорем , термин, часто используемый как синоним). Самым известным из них является стандарт SMT-LIB, [ цитата необходима ], который предоставляет язык, основанный на S-выражениях . Другие обычно поддерживаемые стандартизованные форматы - это формат DIMACS [ необходима ссылка ], поддерживаемый многими логическими программами SAT, и формат CVC [ требуется ссылка ], используемый автоматическим средством доказательства теорем CVC.
Формат SMT-LIB также поставляется с рядом стандартизированных тестов и позволяет проводить ежегодное соревнование между решателями SMT под названием SMT-COMP. Первоначально конкурс проводился во время конференции по компьютерной проверке (CAV), [5] [6], но с 2020 года конкурс проводится в рамках семинара SMT, который связан с Международной объединенной конференцией по автоматизированному мышлению (IJCAR). ). [7]
Приложения
Решатели SMT полезны как для проверки, доказательства правильности программ, тестирования программного обеспечения, основанного на символьном исполнении , так и для синтеза , генерации фрагментов программы путем поиска в пространстве возможных программ. Помимо верификации программного обеспечения, решатели SMT также использовались для вывода типов [8] [9] и для моделирования теоретических сценариев, включая моделирование убеждений участников в контроле над ядерными вооружениями . [10]
Проверка
Для компьютерной проверки компьютерных программ часто используются решатели SMT. Распространенным методом является перевод предусловий, постусловий, условий цикла и утверждений в формулы SMT, чтобы определить, все ли свойства могут выполняться.
Есть много верификаторов, построенных на основе решателя Z3 SMT . Boogie - это язык промежуточной проверки, который использует Z3 для автоматической проверки простых императивных программ. VCC верификатор для одновременного C использует буги, а также Dafny для императивных объектно-ориентированных программ, Чашу для параллельных программ, и Spec # для C #. F * - это язык с зависимой типизацией, использующий Z3 для поиска доказательств; компилятор передает эти доказательства для создания байт-кода, несущего доказательство. Проверка Гадюка инфраструктура кодирует проверки условия для Z3. Библиотека sbv обеспечивает проверку программ Haskell на основе SMT и позволяет пользователю выбирать среди ряда решателей, таких как Z3, ABC, Boolector, CVC4 , MathSAT и Yices.
Также существует множество верификаторов, построенных на основе решателя Alt-Ergo SMT. Вот список зрелых приложений:
- Why3 , платформа для дедуктивной верификации программ, использует Alt-Ergo в качестве основного средства проверки;
- CAVEAT, C-верификатор, разработанный CEA и используемый Airbus; Alt-Ergo был включен в квалификацию DO-178C одного из своих последних самолетов;
- Frama-C , фреймворк для анализа C-кода, использует Alt-Ergo в плагинах Jessie и WP (предназначенных для «дедуктивной проверки программ»);
- SPARK использует CVC4 и Alt-Ergo (за GNATprove) для автоматизации проверки некоторых утверждений в SPARK 2014;
- Atelier-B может использовать Alt-Ergo вместо своего основного прувера (увеличивая успешность с 84% до 98% в тестах ANR Bware project );
- Rodin , фреймворк B-методов, разработанный Systerel, может использовать Alt-Ergo в качестве бэк-энда;
- Cubicle , средство проверки моделей с открытым исходным кодом для проверки свойств безопасности систем перехода на основе массивов.
- EasyCrypt , набор инструментов для анализа реляционных свойств вероятностных вычислений с состязательным кодом.
Многие решатели SMT реализуют общий формат интерфейса, называемый SMTLIB2 (такие файлы обычно имеют расширение « .smt2 »). Инструмент LiquidHaskell реализует верификатор на основе типа уточнения для Haskell, который может использовать любой совместимый с SMTLIB2 решатель, например CVC4, MathSat или Z3.
Анализ и тестирование на основе символьного исполнения
Важным применением решателей SMT является символьное выполнение для анализа и тестирования программ (например, concolic testing ), нацеленных, в частности, на обнаружение уязвимостей безопасности. К важным активно поддерживаемым инструментам в этой категории относятся SAGE от Microsoft Research , KLEE , S2E и Triton . Решатели SMT, которые особенно полезны для приложений с символьным исполнением, включают Z3 , STP , Z3str2 и Boolector .
Смотрите также
- Программирование набора ответов
- Автоматическое доказательство теорем
Заметки
- ^ Барбоза, Ханиэль и др. « Расширение решателей SMT на логику более высокого порядка ». Международная конференция по автоматическому отчислению. Спрингер, Чам, 2019.
- ^ Nieuwenhuis, R .; Oliveras, A .; Тинелли, К. (2006), "Решение теорий SAT и SAT по модулю: от абстрактной процедуры Дэвиса-Патнэма-Логеманна-Ловленда до DPLL (T)", Журнал ACM (PDF) , 53 , стр. 937–977
- ^ Bauer, A .; Пистер, М .; Tautschnig, M. (2007), "Инструментальная поддержка для анализа гибридных систем и моделей", Труды конференции 2007 года по проектированию, автоматизации и тестированию в Европе (DATE'07) , IEEE Computer Society, стр. 1, CiteSeerX 10.1.1.323.6807 , DOI : 10,1109 / DATE.2007.364411 , ISBN 978-3-9810801-2-4, S2CID 9159847
- ^ Fränzle, M .; Herde, C .; Ratschan, S .; Шуберт, Т .; Тейдж, Т. (2007), "Эффективное решение больших нелинейных арифметических систем ограничений со сложной булевой структурой", Специальный выпуск JSAT по интеграции SAT / CP (PDF) , 1 , стр. 209–236
- ^ Барретт, Кларк; де Моура, Леонардо; Пень, Аарон (2005). Этессами, Коуша; Раджамани, Шрирам К. (ред.). "SMT-COMP: Конкурс теорий выполнимости по модулю" . Компьютерная проверка . Конспект лекций по информатике. Берлин, Гейдельберг: Springer: 20–23. DOI : 10.1007 / 11513988_4 . ISBN 978-3-540-31686-2.
- ^ Барретт, Кларк; де Моура, Леонардо; Ранис, Сильвио; Пень, Аарон; Тинелли, Чезаре (2011). Барнер, Шэрон; Харрис, Ян; Кронинг, Даниэль; Раз, Орна (ред.). «Инициатива SMT-LIB и рост SMT» . Аппаратное и программное обеспечение: проверка и тестирование . Конспект лекций по информатике. Берлин, Гейдельберг: Springer: 3–3. DOI : 10.1007 / 978-3-642-19583-9_2 . ISBN 978-3-642-19583-9.
- ^ «СМТ-КОМП 2020» . SMT-COMP . Проверено 19 октября 2020 .
- ^ Хасан, Мостафа и др. "Вывод типа на основе Maxsmt для python 3." Международная конференция по компьютерной проверке. Спрингер, Чам, 2018.
- ^ Loncaric, Calvin, et al. «Практическая основа для объяснения ошибок вывода типов». Уведомления ACM SIGPLAN 51.10 (2016): 781-799.
- ^ Бомонт, Пол; Эванс, Нил; Хут, Майкл; Завод, Том (2015). Пернул, Гюнтер; Я. Райан, Питер; Weippl, Эдгар (ред.). "Анализ уверенности для контроля над ядерным оружием: SMT-абстракции байесовских сетей верований" . Компьютерная безопасность - ESORICS 2015 . Конспект лекций по информатике. Чам: Издательство Springer International: 521–540. DOI : 10.1007 / 978-3-319-24174-6_27 . ISBN 978-3-319-24174-6.
Рекомендации
- С. Барретт, Р. Себастьяни, С. Сешия и С. Тинелли, " Теории выполнимости по модулю ". В Справочнике по выполнимости, т. 185 of Frontiers in Искусственный интеллект и приложения (A Biere, MJH Heule, H van Maaren и T. Walsh, ред.), IOS Press, февраль 2009 г., стр. 825–885.
- Виджай Ганеш (докторская диссертация 2007 г.), Процедуры принятия решений для битовых векторов, массивов и целых чисел , факультет компьютерных наук, Стэнфордский университет, Стэнфорд, Калифорния, США, сентябрь 2007 г.
- Сусмит Джа, Ришикеш Лимай и Санджит А. Сешия. Бивер: Разработка эффективного решателя SMT для бит-векторной арифметики. В материалах 21-й Международной конференции по автоматизированной проверке, стр. 668–674, 2009.
- Р. Э. Брайант, С. М. Герман и М. Н. Велев, " Проверка микропроцессора с использованием эффективных процедур принятия решений для логики равенства с неинтерпретируемыми функциями ", в Аналитических таблицах и связанных с ними методах, стр. 1–13, 1999.
- М. Дэвис и Х. Патнэм, Вычислительная процедура для теории количественной оценки , Журнал Ассоциации вычислительной техники, вып. 7, №, с. 201–215, 1960.
- М. Дэвис, Дж. Логеманн, Д. Лавленд, Машинная программа для доказательства теорем , Связь ACM, т. 5, вып. 7. С. 394–397, 1962.
- Д. Кроенинг и О. Стрихман, Процедуры принятия решений - алгоритмическая точка зрения (2008), Springer (серия теоретических информатики) ISBN 978-3-540-74104-6 .
- Г.-Дж. Нам, К.А. Сакаллах и Р. Рутенбар, Новый подход к детальной маршрутизации ПЛИС с помощью логической удовлетворенности на основе поиска , IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 21, нет. 6. С. 674–684, 2002.
- SMT-LIB: Библиотека теорий по модулю выполнимости
- SMT-COMP: Конкурс теорий по модулю выполнимости
- Процедуры принятия решений - алгоритмическая точка зрения
- Р. Себастьяни, Теории ленивой выполнимости по модулю , Dipartimento di Ingegneria e Scienza dell'Informazione, Университет Тренто, Италия, декабрь 2007 г.
- Д.Юричев, Краткое знакомство с решателями SAT / SMT и символьным исполнением
Эта статья адаптирована из колонки в электронном информационном бюллетене ACM SIGDA, подготовленной профессором Каремом Сакаллахом . Исходный текст доступен здесь