Reparación eficiente de estructuras de datos en tiempo de ejecución basada en SAT

Abstract

Las fallas de un programa pueden producir estados internos inconsistentes, cuya propagación puede provocar la terminación abrupta del programa, la pérdida de datos del usuario, la incapacidad de realizar alguna tarea, etc. La reparación de estructuras de datos consiste en reemplazar estos estados inconsistentes por estructuras generadas a partir de especificaciones formales, utilizando algún procedimiento de decisión, que permitan al programa continuar su ejecución sin mayores problemas. En este trabajo se presenta un enfoque para resolver este problema basado en SAT solving, cuya característica distintiva es el aprovechamiento de dos técnicas del estado del arte para mejorar su eficiencia y escalabilidad: el uso de rotura de simetrías y de cotas ajustadas. La evaluación experimental preliminar realizada muestra que nuestro enfoque es más eficiente y es capaz de lidiar con estructuras de mayor complejidad que técnicas relacionadas.