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

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

Основная терминология [ править ]

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

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

Выразительная сила [ править ]

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

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

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

Решатель приближается [ править ]

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

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

SMT для неразрешимых теорий [ править ]

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

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

где

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

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

Примерами решателей SMT, обращающихся к булевым комбинациям атомов теории из неразрешимых арифметических теорий над действительными числами, являются ABsolver ^{[3], в} котором используется классическая архитектура DPLL (T) с пакетом нелинейной оптимизации в качестве (обязательно неполного) решателя теории подчиненных функций, и iSAT [1] , основанный на объединении DPLL-решения SAT и распространения интервальных ограничений, который называется алгоритмом iSAT. ^[4]

Решатели[ редактировать ]

В таблице ниже приведены некоторые функции многих доступных решателей 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), ^{[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. ЗСОБиблиотека обеспечивает проверку программ 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 .

См. Также [ править ]

• Программирование набора ответов
• Автоматическое доказательство теорем

Заметки [ править ]

Ссылки [ править ]

• С. Барретт, Р. Себастьяни, С. Сешия и С. Тинелли, " Теории выполнимости по модулю ". В Справочнике по выполнимости, т. 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, подготовленной профессором Каремом Сакаллахом . Исходный текст доступен здесь