The RISC ProofNavigator

October 29, 2009: RISC ProofNavigator 1.17 (fixes bug with parentheses of arithmetic expressions, turns off implicit REAL->INT conversion)

The RISC ProofNavigator is an interactive proof assistant for supporting formal reasoning about computer programs and computing systems, see the README file; 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.

[A Proof]
Click on an image to enlarge it. To see the proof, use a browser that understands XHTML+MathML, for instance Mozilla Firefox.

MS Windows Users: You can download a pre-configured virtual Linux machine (for the free VirtualBox virtualization software) with the RISC ProofNavigator for execution under MS Windows.

Virtual Machine with the RISC ProofNavigator

RISC Users: The ProofNavigator is installed in the RISC environment. To start the software, execute

module load ProofNavigator
ProofNavigator &

Download ProofNavigator 1.17

This is a binary distribution for GNU/Linux x86 computers (32-bit or 64-bit).
See the files README, INSTALL, CHANGES, and COPYING.

Tutorial and Manual [HTML | PDF]

This is the user documentation for the software.

The Java API

This is the interface documentation of the program classes.

Subversion Repository

This is a web interface to the Subversion repository that holds the source code of the program. The repository can be read anonymously by any Subversion client from the URL