¿Cuáles son las diferencias entre la ejecución simbólica y los solucionadores SAT?

Question

Tengo entendido que la ejecución simbólica solo se ocupa de rutas específicas y malos patrones, mientras que los solucionadores SAT, o las teorías del módulo de satisfacibilidad en general, proporcionan un análisis mucho más sólido del programa.

¿Alguien podría validar la afirmación anterior y explicar (brevemente) las diferencias entre estas dos metodologías de verificación formales?

Answer 1

TL;DR: Se diferencian en sus entradas y salidas básicas.Los solucionadores de SAT y SMT no saben qué son los programas;son herramientas que responden sí o no preguntas sobre fórmulas matemáticas.La ejecución simbólica, por otro lado, es un método para analizar programas.La ejecución simbólica suele depender de solucionadores SAT y SMT, pero no al revés.

---

Solucionadores SAT y SMT No tienen nada que ver directamente con los programas.En cambio, un solucionador SAT o SMT toma como entrada una "fórmula" descrita matemáticamente y responde, aproximadamente, si es verdadera o falsa.(A menudo se permite una tercera opción, desconocido, para los casos en los que el solucionador no puede encontrar una respuesta).

Por ejemplo, una posible entrada a un solucionador SAT es (a and not b) or (not a and c).Es decir, es una fórmula matemática, donde a, b, y c Aquí hay constantes booleanas (0 o 1).Se supone que el solucionador SAT decide si es posible que la fórmula sea verdadera, eligiendo valores de a, b, y c.Los solucionadores SMT son similares, pero a, b, y c sería reemplazado por fórmulas más complejas usando números enteros, cadenas, funciones, etc., por ejemplo x + 3 = y^2.

---

Ejecución simbólica es una forma elegante de ejecutar un programa, pero no cómo se pretendía ejecutar el programa.En lugar de ello, el programa se ejecuta utilizando los llamados valores "simbólicos", que son algo así como marcadores de posición.Para ver un ejemplo de lo que eso significa, supongamos que tengo una función como f(x) = if x > 0 then 1 else 0.Ahora, normalmente, ejecutaría el programa ingresando, digamos, 3, y obten f(3) = 1, desde 3 es mayor que 0.Con la ejecución simbólica, ejecuto el programa ingresando una variable de marcador de posición, input, y evalúo el programa para obtener dos casos:cualquiera input > 0 and answer = 1 o input <= 0 and answer = 0.Esto puede parecer inútil, pero acaba siendo una poderosa forma de analizar programas.

---

La conexión entre los dos La razón es que la ejecución simbólica a menudo depende de solucionadores SMT durante la ejecución, para determinar si una determinada ruta es realmente posible o si debe descartarse.Por ejemplo, se podría utilizar un solucionador SMT para determinar si input <= 0 and answer = 0 es posible (la respuesta es sí, por ejemplo si input = 0).De esta manera, SMT es una especie de "fuerza impulsora" detrás de lo que hace factible la ejecución simbólica.