RISC ProofNavigator

An Interactive Proof Assistant for Program/System Verification

Authors

Wolfgang Schreiner

Software URL

Go to Website
The RISC ProofNavigator is an interactive proof assistant for supporting formal reasoning about computer programs and computing systems, see the README file and this short paper for the main ideas; it is the core reasoning component of the RISC ProgramExplorer. The software runs on computers with x86-compatible processors under the GNU/Linux operating system; it is freely available under the terms of the GNU GPL.