Título: Buscador de Modelos Acotados para el demostrador de teoremas PVS

Resumen:

La demostración de teoremas en un ambiente interactivo, donde la guía de una persona es necesaria, es usualmente una actividad tediosa y muy propensa a fallas. Pequeños errores en la declaración original pueden provocar la pérdida de una cantidad considerable de tiempo por «forzar» al usuario a lidiar con la inútil tarea de intentar probar una propiedad que no es válida. Estos errores tienen un amplio rango de orígenes, pero son mucho más probables de ocurrir cuando la actividad de demostración forma parte de desarrollos formales de gran complejidad. El Sistema de Verificación de Prototipos (conocido como PVS por su nombre en inglés) es un framework mecanizado para la especificación y verificación formal de artefactos en Lógica de Alto Orden.

Por otro lado, los analizadores automáticos han presentado un crecimiento pronunciado respecto a su poder de alcance en las últimas décadas. Nuevas técnicas pueden ser aplicadas ahora a problemas que no podían ser tratados en el pasado. Un ejemplo de esos analizadores es Kodkod: un buscador de modelos para Lógica Relacional de Primer Orden que, entre otros usos, sirve como backend para el Alloy Analyzer, desarrollado por el Massachusetts Institute of Technology.

En esta tesis se presentan los primeros pasos para desarrollar un buscador de contraejemplos para PVS basado en Kodkod. Se propone un enfoque preliminar para una de las características fundamentales para el método propuesto, que es la traducción entre un fragmento relevante del lenguaje de PVS y el de Kodkod. Además discutimos sobre el campo de aplicación de esta técnica automática en el contexto de la demostración de teoremas, sobre sus limitaciones y otras técnicas similares.