Premios HVC de verificación a la comunidad SMT (Satisfiability Modulo Theories)

PorJosé A. Alonso

Los premios HVC (Haifa Verification Conference) se conceden a los trabajos más prometedores en la campos de verificación y prueba de software y hardware. Este año los premios HVC 2010 le han sido otorgados a los promotores de la comunidad de satisfacibilidad módulo teorías (en inglés, Satisfiability Modulo Theories (SMT) personalisados en

Con el premio se reconoce el papel que han jugado en la creación y promoción de la comunidad SMT, principalmente con los siguientes proyectos:

  • el formato SMT-lib definido por Ranise y Tinelli como un lenguaje común para especificar pruebas para SMT. La vesión actual es obra de Barrett, Stump y Tinelli.
  • el repositorio SMT-LIB en el que se recopilan pruebas para SMT. Actualmente contiene 93.480 pruebas. Los principales gestores del repositorio son Barrett, Deters y Tinelli.
  • la competición SMT-COMP en la que compiten anualmente sistemas SMT. Los actuales organizadores son Clark Barrett, Morgan Deters, Albert Oliveras y Aaron Stump.
  • el SMT-Exec (The Satisfiability Modulo Theories Execution Service) que es un servicio web que permite realizar experimentos en línea son sistemas SMT sobre las pruebas de SMT-lib. Los promotores de SMT-Exec son Deters y Stump.

Además, se reconoce el éxito académico e industrial dee la satisfacibilidad módulo teoría. El éxito académico de SMT puede apreciarse en los artículos publicados. Actualmente se encuentran 1100 artículos en Google Scholar al buscar “Satisfiability modulo theories”. El éxito industrial de SMT puede apreciarse en las empresas que usan sistemas SMT.

  • Microsoft usa el Z3 en herramientas de análisis de programas,
  • Intel usa MathSAT y Boolector para la verificación de hardware,
  • otras empresas que usan sistema SMT son Galois Connection, Praxis, GrammaTech, NVIDIA, Synopsys , Mathworks, Dassault Aviation, etc.

Los sistemas SMT se están integrando en los demostradores de teoremas. Por ejemplo, Isabelle integra Z3 y PVS integra Yices.

Una buena introducción a la satisfacibilidad módulo teorías es el capítulo de Clark Barrett, Roberto Sebastiani, Sanjit Seshia y Cesare Tinelli Satisfiability Modulo Theories en el Handbook on Satisfiability (IOS Press, Febrero de 2009).