A Verification System
Author
Bonyadlou, Rasa
Term
4. term
Education
Publication year
2003
Abstract
Prototyping Verification System (PVS), udviklet af Stanford Research Institute (SRI), er en interaktiv bevisassistent (theorem prover): software, der hjælper brugere med at skrive præcise, matematiske beskrivelser af systemer (formelle specifikationer) og kontrollere beviser om dem. PVS arbejder i typet højereordens logik, et strengt formelt sprog med typer, der kan udtrykke funktioner og egenskaber ved funktioner. Systemet tilbyder et integreret miljø til at udvikle, analysere og dokumentere specifikationer, teorier og beviser. Projektet har to mål: at forklare, hvordan PVS fungerer, og at genimplementere systemet i Java.
The Prototyping Verification System (PVS), developed by Stanford Research Institute (SRI), is an interactive theorem prover: software that helps users write precise, mathematical descriptions of systems (formal specifications) and check proofs about them. PVS works in typed higher-order logic, a rigorous language with types that can express functions and properties of functions. It provides an integrated environment to develop, analyze, and document specifications, theories, and proofs. This project has two goals: to explain how PVS works and to re-implement the system in Java.
[This abstract was generated with the help of AI]
Documents