¿Cómo se puede asegurar que un app de nuestro móvil no accede a datos incorrectos, que un programa en un ordenador se bloquee inesperadamente o que el software que se ejecuta en un coche no tiene errores fatales que pueden derivar en la pérdida de vidas humanas – antes de que eso suceda y sin tener que instalar y probar ese software o esa app en cientos o miles de dispositivos? Esa es la misión de las técnicas de verificación de software: probar que un programa no tiene errores sin necesitar ejecutar ese programa en su entorno real. Esa es una de las líneas de investigación del Instituto IMDEA Software, uno de los siete institutos IMDEA de investigación promovidos y financiados por la Comunidad de Madrid.
La verificación de software conforma un área de investigación de incuestionable importancia a medida que la sociedad es cada vez más dependiente de su correcto funcionamiento: los errores de software pueden costar grandes pérdidas económicas e incluso vidas. Aunque el objetivo de la verificación de software ha existido desde el principio de la ciencia informática, el creciente uso de verificadores en la industria de creación de software ha supuesto un gran reto para su desarrollo, debido a limitaciones científicas fundamentales, obstáculos prácticos en ingeniería, y el desafío de superar ambos de forma simultánea.
La International Competition on Software Verification (SV-COMP) es una iniciativa internacional para potenciar la creación de nuevos métodos, tecnologías, y herramientas para la verificación automática de software informático: una competición abierta donde los mejores investigadores en informática del mundo enfrentan a sus verificadores intentando probar automáticamente la corrección de una serie de programas, o encontrar errores en los mismos.
Este año ha tenido lugar la 4ª edición de este evento, cada año más competitivo, donde se recibieron propuestas de 22 de las más destacadas instituciones de investigación a nivel global, como por ejemplo New York University, la École Normale Supérieure (ENS) de Paris, la Universidad de Friburgo, la Universidad Tsinghua, Microsoft Research Institute, y el Instituto IMDEA Software. La competición se desarrolla en trece categorías diferentes sobre problemas de verificación de software.
En la competición se le dan problemas (programas informáticos cuya exactitud ha de ser comprobada) a otros programas, llamados “verificadores”. Los verificadores clasifican estos problemas como “correcto”, “incorrecto”, o “desconocido” dentro de un tiempo máximo de quince minutos por problema. El método de puntuación se establece en relación a la precisión en la clasificación. Dentro de cada tipo de problema, los verificadores con las puntuaciones más altas son premiados con medallas de oro, plata, y bronce.
El verificador SMACK+Corral, presentado por el Instituto IMDEA Software y realizado en colaboración con la Universidad de Utah y Microsoft Research, fue premiado con medallas en 4 categorías – dos de oro, una de plata, y una de bronce – situándose entre los mejores de toda la competición: sólo otra participación logró más medallas de oro. SMACK+Corral une dos verificadores desarrollados como código abierto; el desarrollo de SMACK está liderado por Michael Emmi, del Instituto IMDEA Software, y Zvonimir Rakamaric, de la Universidad de Utah y Corral lo está por Akash Lal y Shaz Qadeer, de Microsoft Research. Los dos verificadores trabajan de manera conjunta para conformar una herramienta más potente que cualquiera de ellos por separado.
El anuncio oficial de los ganadores de la competición tendrá lugar en un evento a celebrar en Londres el 13 de Abril de 2015 como parte del 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).
Más información disponible en la página web de SV-COMP 2015.
