The RISC ProofNavigator

From this page you can download the code of the original version of the RISC ProofNavigator. This code is only kept for archival; it is superseded by the newer version of the RISC ProofNavigator which is integrated in the RISC ProgramExplorer. Just download the RISC ProgramExplorer and rename the script to "ProofNavigator"; the script will then start the RISC ProgramExplorer in a mode that presents the pure RISC ProofNavigator interface. The manual linked on this page essentially also describes the use of the new version of the RISC ProofNavigator (small differences are listed in the manual of the RISC ProgramExplorer).

July 7, 2010: RISC ProofNavigator 1.18 (packaged with SWT 3.6)

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.

[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 new (maintained) version of the software included in the RISC ProgramExplorer, execute

module load ProgramExplorer
ProofNavigator &

To start the original (unmaintained) version of the software, execute

module load ProofNavigator
ProofNavigator &

Download ProofNavigator 1.18

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