RISC JKU

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
svn://svn.risc.uni-linz.ac.at/schreine/FM-RISC
Third Party Software
The following third-party software is used by the ProofNavigator (see the README file for more details):
CVC Lite 2.0 (local copy of version 2.0)
RIACA OpenMath Library 2.0 (local copy)
General Purpose Hash Function Algorithms Library (local copy)
ANTLR 2.7.6b2 (local copy)
Eclipse Standard Widget Toolkit 3.5 (local copy for GNU/Linux x86 32 bit and 64 bit)
Mozilla Firefox or SeaMonkey (README, local copy)
GIMP Toolkit GTK+ 2.X
Sun JDK 6
Tango Icon Library (local copy)
Talks, Reports, Publications
Collected information on the RISC ProofNavigator.
TWiki
A project collaboration area.

Wolfgang Schreiner
Last modified: Thu Sep 15 18:08:25 CEST 2011