Каковы различия между символическим выполнением и решателями SAT?

Question

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

Может ли кто-нибудь подтвердить приведенное выше утверждение и (вкратце) объяснить различия между этими двумя формальными методологиями проверки?

Answer 1

ТЛ;ДР: Они различаются по основному вводу и выводу.Решатели SAT и SMT не знают, что такое программы;это инструменты, которые отвечают «да» или «нет» на вопросы о математических формулах.Символическое выполнение, с другой стороны, является методом анализа программ.Символическое выполнение обычно зависит от решателей SAT и SMT, но не наоборот.

---

Решатели SAT и SMT не имеют прямого отношения к программам.Вместо этого решатель SAT или SMT принимает на вход математически описанную «формулу» и примерно отвечает, истинна она или ложна.(Часто допускается третий вариант, неизвестный, для случаев, когда решатель не может найти ответ.)

Например, возможные входные данные для решателя SAT: (a and not b) or (not a and c).То есть это математическая формула, где a, b, и c вот логические константы (0 или 1).Решающая программа SAT должна решить, может ли формула быть верной, выбирая значения a, b, и c.Решатели SMT похожи, но a, b, и c будут заменены более сложными формулами, использующими целые числа, строки, функции и т. д., например x + 3 = y^2.

---

Символическое исполнение — это необычный способ запуска программы, но не тот, для которого она предназначена.Вместо этого программа запускается с использованием так называемых «символических» значений, которые представляют собой своего рода заполнители.Для примера того, что это значит, предположим, что у меня есть функция типа f(x) = if x > 0 then 1 else 0.Обычно я запускаю программу, вводя, скажем, 3, и получить f(3) = 1, с 3 больше, чем 0.При символическом выполнении я запускаю программу, вводя переменную-заполнитель: input, и я оцениваю программу, чтобы получить два случая:или input > 0 and answer = 1 или input <= 0 and answer = 0.Это может показаться бесполезным, но в конечном итоге это мощный способ анализа программ.

---

Связь между двумя заключается в том, что символическое выполнение часто полагается на решатели SMT во время выполнения, чтобы выяснить, действительно ли возможен определенный путь или его следует отбросить.Например, решатель SMT можно использовать, чтобы определить, input <= 0 and answer = 0 возможно (ответ – да, например, если input = 0).Таким образом, SMT является своего рода «движущей силой», делающей возможным символическое исполнение.