Was sind die Unterschiede zwischen symbolischer Ausführung und SAT-Lösern?

Question

Nach meinem Verständnis befasst sich die symbolische Ausführung nur mit bestimmten Pfaden und fehlerhaften Mustern, während SAT-Löser oder Erfüllbarkeits-Modulo-Theorien im Allgemeinen eine viel robustere Analyse des Programms liefern.

Könnte jemand die obige Aussage bestätigen und (kurz) die Unterschiede zwischen diesen beiden formalen Verifizierungsmethoden erklären?

Answer 1

TL;DR: Sie unterscheiden sich in ihrem grundlegenden Input und Output.SAT- und SMT-Löser wissen nicht, was Programme sind;Es handelt sich um Werkzeuge, die Fragen zu mathematischen Formeln mit Ja oder Nein beantworten.Die symbolische Ausführung hingegen ist eine Methode zur Analyse von Programmen.Die symbolische Ausführung basiert normalerweise auf SAT- und SMT-Lösern, nicht jedoch umgekehrt.

---

SAT- und SMT-Löser haben nicht direkt etwas mit Programmen zu tun.Stattdessen verwendet ein SAT- oder SMT-Löser als Eingabe eine mathematisch beschriebene „Formel“ und antwortet grob, ob sie wahr oder falsch ist.(Oft ist eine dritte Option zulässig, Unbekannt, für Fälle, in denen der Löser keine Antwort finden kann.)

Eine mögliche Eingabe für einen SAT-Löser ist beispielsweise (a and not b) or (not a and c).Das heißt, es ist eine mathematische Formel, wo a, b, Und c Hier sind boolesche (0 oder 1) Konstanten.Der SAT-Löser soll entscheiden, ob die Formel wahr sein kann, indem er Werte von auswählt a, b, Und c.SMT-Löser sind ähnlich, aber a, b, Und c durch komplexere Formeln ersetzt werden, die beispielsweise ganze Zahlen, Zeichenfolgen, Funktionen usw. verwenden x + 3 = y^2.

---

Symbolische Hinrichtung ist eine ausgefallene Art, ein Programm auszuführen, aber nicht die Art und Weise, wie das Programm ausgeführt werden sollte.Stattdessen wird das Programm mit sogenannten „symbolischen“ Werten ausgeführt, die so etwas wie Platzhalter sind.Als Beispiel dafür, was das bedeutet, nehmen wir an, ich habe eine Funktion wie f(x) = if x > 0 then 1 else 0.Normalerweise würde ich das Programm ausführen, indem ich beispielsweise Folgendes eingebe: 3, und bekomme f(3) = 1, seit 3 ist größer als 0.Bei der symbolischen Ausführung führe ich das Programm aus, indem ich eine Platzhaltervariable eingebe. input, und ich bewerte das Programm, um zwei Fälle zu erhalten:entweder input > 0 and answer = 1 oder input <= 0 and answer = 0.Dies mag nutzlos erscheinen, ist aber letztendlich eine leistungsstarke Methode zur Analyse von Programmen.

---

Die Verbindung zwischen den beiden liegt darin, dass die symbolische Ausführung während der Ausführung häufig auf SMT-Löser angewiesen ist, um herauszufinden, ob ein bestimmter Pfad tatsächlich möglich ist oder ob er verworfen werden sollte.Beispielsweise könnte ein SMT-Löser verwendet werden, um festzustellen, ob input <= 0 and answer = 0 ist möglich (die Antwort ist ja, zum Beispiel wenn input = 0).Auf diese Weise ist SMT sozusagen die „treibende Kraft“ dahinter, was die symbolische Ausführung möglich macht.