Quelles sont les différences entre l'exécution symbolique et les solveurs SAT ?

Question

Je crois comprendre que l'exécution symbolique ne traite que des chemins spécifiques et des mauvais modèles, tandis que les solveurs SAT, ou les théories modulo de satisfiabilité en général, fournissent une analyse beaucoup plus robuste du programme.

Quelqu'un pourrait-il valider la déclaration ci-dessus et expliquer (brièvement) les différences entre ces deux méthodologies de vérification formelle ?

Answer 1

TL;DR : Ils diffèrent par leurs entrées et sorties de base.Les solveurs SAT et SMT ne savent pas ce que sont les programmes ;ce sont des outils qui répondent par oui ou par non à des questions sur les formules mathématiques.L’exécution symbolique, quant à elle, est une méthode d’analyse de programmes.L'exécution symbolique repose généralement sur les solveurs SAT et SMT, mais pas l'inverse.

---

Solveurs SAT et SMT n'ont rien à voir directement avec les programmes.Au lieu de cela, un solveur SAT ou SMT prend en entrée une « formule » mathématiquement décrite et répond, grossièrement, si elle est vraie ou fausse.(Souvent, une troisième option est autorisée, inconnu, pour les cas où le solveur ne parvient pas à trouver une réponse.)

Par exemple, une entrée possible dans un solveur SAT est (a and not b) or (not a and c).Autrement dit, c'est une formule mathématique, où a, b, et c voici les constantes booléennes (0 ou 1).Le solveur SAT est censé décider s'il est possible que la formule soit vraie, en choisissant les valeurs de a, b, et c.Les solveurs SMT sont similaires, mais a, b, et c serait remplacé par des formules plus complexes utilisant des entiers, des chaînes, des fonctions, etc., par exemple x + 3 = y^2.

---

Exécution symbolique est une façon sophistiquée d'exécuter un programme, mais pas la manière dont le programme est censé être exécuté.Au lieu de cela, le programme est exécuté en utilisant des valeurs dites « symboliques », qui sont un peu comme des espaces réservés.Pour un exemple de ce que cela signifie, supposons que j'ai une fonction comme f(x) = if x > 0 then 1 else 0.Maintenant, normalement, j'exécuterais le programme en saisissant, disons : 3, et obtenir f(3) = 1, depuis 3 est supérieur à 0.Avec une exécution symbolique, j'exécute le programme en saisissant une variable d'espace réservé, input, et j'évalue le programme pour obtenir deux cas :soit input > 0 and answer = 1 ou input <= 0 and answer = 0.Cela peut sembler inutile, mais cela s’avère être un moyen puissant d’analyser les programmes.

---

Le lien entre les deux est que l'exécution symbolique s'appuie souvent sur des solveurs SMT pendant l'exécution, pour déterminer si un certain chemin est réellement possible ou s'il doit être ignoré.Par exemple, un solveur SMT pourrait être utilisé pour déterminer si input <= 0 and answer = 0 est possible (la réponse est oui, par exemple si input = 0).De cette manière, SMT est en quelque sorte la « force motrice » derrière ce qui rend l’exécution symbolique réalisable.