Sistema de verificación de prototipos

El Sistema de Verificación de Prototipos ( PVS ) es un lenguaje de especificación integrado con herramientas de soporte y un demostrador automático de teoremas , desarrollado en el Laboratorio de Ciencias de la Computación de SRI International en Menlo Park, California .

PVS se basa en un núcleo que consiste en una extensión de la teoría de tipos de Church con tipos dependientes , y es fundamentalmente una lógica clásica de orden superior tipada. Los tipos base incluyen tipos no interpretados que puede introducir el usuario, y tipos integrados como los booleanos, enteros, reales y ordinales. Los constructores de tipos incluyen funciones, conjuntos, tuplas, registros, enumeraciones y tipos de datos abstractos. Los subtipos de predicados y los tipos dependientes se pueden usar para introducir restricciones; estos tipos restringidos pueden generar obligaciones de prueba (llamadas condiciones de corrección de tipos o TCC) durante la verificación de tipos. Las especificaciones de PVS están organizadas en teorías parametrizadas.

El sistema está implementado en Common Lisp y se distribuye bajo la Licencia Pública General de GNU (GPL).

• Métodos formales
• Lista de asistentes de prueba
• Rosetta-lang

• Owre , Shankar y Rushby , 1992. PVS: Un sistema de verificación de prototipos . Publicado en las actas de la conferencia CADE 11 .

• Sitio web de PVS en el Laboratorio de Ciencias de la Computación de SRI International.
• Resumen de PVS por John Rushby en la base de datos de razonamiento mecanizado de Michael Kohlhase y Carolyn Talcott.
• PVSgym es un entorno de aprendizaje por refuerzo para PVS