Sistema de verificación de prototipos

Captura de pantalla de PVS

El Sistema de Verificación de Prototipos ( PVS ) es un lenguaje de especificación integrado con herramientas de soporte y un comprobador de teoremas automatizado , 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 tipado. Los tipos base incluyen tipos no interpretados que pueden ser introducidos por el usuario, y tipos incorporados como 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 utilizar para introducir restricciones; estos tipos restringidos pueden incurrir en obligaciones de prueba (denominadas condiciones de corrección de tipo o TCC) durante la verificación de tipos. Las especificaciones PVS están organizadas en teorías parametrizadas.

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

Ver también

Métodos formales

Referencias

Owre , Shankar y Rushby , 1992. PVS: A Prototype Verification System . Publicado en las actas de la conferencia CADE 11 .

enlaces externos

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

Este artículo relacionado con el lenguaje de programación es un código auxiliar . Puedes ayudar a Wikipedia expandiéndolo .

Este artículo relacionado con la lógica es un fragmento . Puedes ayudar a Wikipedia expandiéndolo .