verification - Límites de los solucionadores de SMT

formal-methods theorem-proving

Question

Tradicionalmente, la mayoría de los trabajos con lógica computacional eran proposicionales, en cuyo caso usaba un solucionador SAT (satisfacción booleana), o de primer orden, en cuyo caso utilizaba un verificador de teoremas de primer orden.

En los últimos años, se ha avanzado mucho en los solucionadores SMT (teoría de modulo de satisfacción), que básicamente aumentan la lógica proposicional con las teorías de la aritmética, etc .; John Rushby, de SRI International, llega tan lejos como para llamarlos una tecnología disruptiva.

¿Cuáles son los ejemplos prácticos más importantes de problemas que se pueden manejar en la lógica de primer orden pero que SMT aún no puede manejar? Más particularmente, ¿qué tipo de problemas surgen que SMT no puede manejar en el dominio de verificación de software?

Answer 1

Los solucionadores de SMT no son más poderosos que los de SAT. Todavía se ejecutarán en tiempo exponencial o estarán incompletos para los mismos problemas en SAT. La ventaja de SMT es que muchas cosas que son obvias en SMT pueden tomar mucho tiempo para que un solucionador de satélites equivalente pueda redescubrirse.

Por lo tanto, con la verificación de software como ejemplo, si usa un solucionador SMT QF BV (teoría de cuantificadores libres de bits), el solucionador SMT sabrá que (a + b = b + a) en un nivel de palabra, en cambio, A un solucionador de SAT le puede llevar mucho tiempo demostrar que utiliza los valores booleanos individuales.

Por lo tanto, para la verificación de software, puede hacer fácilmente problemas en la verificación de software que serían difíciles para cualquier solucionador de SMT o SAT.

Primero, los bucles deben desenrollarse en QF BV, lo que significa que prácticamente debe limitar lo que el solucionador verifica. Si se permitieran los cuantificadores, se convierte en un problema de PSPACE completo, no solo NP-completo.

En segundo lugar, los problemas que se consideran difíciles en general son fáciles de codificar en QF BV. Por ejemplo, puede escribir un programa de la siguiente manera:

void run(int64_t a,int64_t b)
{
a * b == <some large semiprime>;
assert (false);
}

Ahora, por supuesto, el solucionador de SMT probará fácilmente que ocurrirá aserción (falso), pero tendrá que proporcionar un ejemplo de contador, que le dará las entradas a,b . Si establece <some large number> en un semiprime RSA, entonces simplemente invirtió la multiplicación ... ¡también conocido como factorización de enteros! Por lo tanto, esto probablemente será difícil para cualquier solucionador de SMT, y demuestra que la verificación del software es un problema difícil en general (a menos que P = NP, o al menos la factorización de enteros sea fácil). Dichos solucionadores de SMT son solo una ventaja para los que resuelven SAT al vestir todo con un lenguaje más fácil de escribir y más fácil de razonar.

Los solucionadores de SMT que resuelven teorías más avanzadas son necesariamente incompletos o incluso más lentos que los de SAT, porque intentan resolver problemas más difíciles.

Ver también:

• Curiosamente, el solucionador Beaver SMT traduce QF BV a CNF y puede usar un solucionador SAT como servicio de fondo.
• Klee que puede llevar un programa compilado a LLVM IR (representación intermedia), busca errores y encuentra ejemplos contrarios a aseveraciones, etc. Si encuentra un error, puede dar un ejemplo contrario a la corrección (le dará entrada). que reproducirá el error).