Un Estudio de Transferibilidad de la Verificación de Modelos de Hardware Basada en Interpolación para la Verificación de Software

Asegurar la corrección de los sistemas de computación es fundamental para nuestra sociedad y economía, y la verificación formal es una clase de técnicas que abordan este problema con rigor matemático. Los investigadores han inventado numerosos algoritmos para probar automáticamente si un modelo computacional, por ejemplo, un programa de software o un circuito digital de hardware, satisface su especificación. En las últimas dos décadas, la interpolación de Craig se ha utilizado ampliamente tanto en la verificación de hardware como de software. A pesar de las similitudes en la base teórica entre la verificación de hardware y software, los trabajos anteriores suelen evaluar algoritmos basados en interpolación en solo un tipo de tareas de verificación (por ejemplo, ya sea circuitos o programas), por lo que las conclusiones de estos estudios no necesariamente se transfieren a diferentes tipos de tareas de verificación. Para investigar la transferibilidad de las conclusiones de la investigación del hardware al software, adoptamos dos enfoques de alto rendimiento de la verificación de modelos de hardware basada en interpolación: (1) Verificación de Modelos Basada en Secuencias de Interpolación (Vizel y Grumberg, 2009) y (2) Análisis de Alcance Adelante-Atrás entrelazado utilizando Interpolantes (Vizel, Grumberg y Shoham, 2013), para la verificación de software. Implementamos los algoritmos propuestos por las dos publicaciones en el verificador de software CPAchecker, porque tiene una adopción de verificación de software del primer algoritmo basado en interpolación para la verificación de modelos de hardware de 2003, que las dos publicaciones utilizan como base de comparación. Para evaluar si las afirmaciones en las dos publicaciones se trasladan a la verificación de software, llevamos a cabo un experimento extenso en el conjunto de tareas de verificación de seguridad más grande disponible públicamente para el lenguaje de programación C. Nuestros resultados experimentales muestran que las características importantes de los dos enfoques para la verificación de modelos de hardware son transferibles a la verificación de software, y que la adopción de algoritmos interdisciplinarios es beneficiosa, ya que los enfoques adoptados de la verificación de modelos de hardware pudieron abordar tareas que no podían ser resueltas por los métodos existentes. Este trabajo consolida el conocimiento en verificación de hardware y software y proporciona implementaciones de código abierto para mejorar la comprensión de los algoritmos basados en interpolación comparados.