Aprovechando al Máximo los Contraejemplos de BMC

El valor de los contraejemplos en la verificación de modelos para depurar programas (y especificaciones) es ampliamente reconocido. Desafortunadamente, los verificadores de modelos acotados a menudo producen contraejemplos que son difíciles de entender debido a los valores elegidos por un solucionador SAT. Este documento presenta dos enfoques para hacer un mejor uso de los contraejemplos de BMC. La primera contribución es una nueva noción de minimización de contraejemplos que minimiza los valores con respecto al sistema de tipos del lenguaje que se está verificando, en lugar de a nivel de variables SAT. Se presentan y comparan enfoques codiciosos y óptimos para el problema de minimización. La segunda contribución extiende un enfoque de explicación de errores basado en BMC para hipotetizar automáticamente causas del error en un contraejemplo. Estas hipótesis (en términos de relaciones entre variables) pueden ser verificadas automáticamente para determinar si existe una dependencia causal. Los resultados experimentales muestran que se pueden determinar automáticamente causas para errores en programas interesantes de ANSI C.