Algoritmos de Verificación para Verificadores de Lógica de Separación Automatizados

La mayoría de los verificadores de programas automatizados para lógica de separación utilizan ejecución simbólica o generación de condiciones de verificación para extraer obligaciones de prueba, que luego se entregan a un solucionador SMT. Los algoritmos de verificación existentes están diseñados para ser sólidos, pero difieren en rendimiento y completitud. Estas características también pueden depender de los programas y propiedades a verificar. En consecuencia, los desarrolladores y usuarios de verificadores de programas deben seleccionar un algoritmo de verificación cuidadosamente para su dominio de aplicación. Tomar una decisión informada requiere una comparación sistemática de las características de rendimiento y completitud de los algoritmos de verificación utilizados por los verificadores de lógica de separación modernos, pero tal comparación no existe. Este documento describe cinco algoritmos de verificación para lógica de separación, tres de los cuales se utilizan en herramientas existentes y dos algoritmos novedosos que combinan características de los algoritmos existentes de ejecución simbólica y generación de condiciones de verificación. Una evaluación detallada de las implementaciones de estos cinco algoritmos en la infraestructura Viper evalúa su rendimiento y completitud para diferentes clases de programas de entrada. Basado en los resultados experimentales, identificamos portafolios candidatos de algoritmos que maximizan la completitud y el rendimiento.