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
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.
Click on an image to enlarge it.
To see the proof, use a browser that understands XHTML+MathML, for
MS Windows Users: You can download a pre-configured
virtual Linux machine
(for the free VirtualBox
with the RISC ProofNavigator for execution under MS Windows.
Virtual Machine with the
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
To start the original (unmaintained) version of the software, execute
module load ProofNavigator
- Download ProofNavigator
- This is a binary distribution for GNU/Linux x86 computers (32-bit or 64-bit).
See the files README, INSTALL,
- 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.
- 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
- 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
- Mozilla Firefox or
SeaMonkey (README, local
- GIMP Toolkit GTK+ 2.X
- Sun JDK 6
- Tango Icon Library (local copy)
- Talks, Reports, Publications
- Collected information on the RISC ProofNavigator.
- A project collaboration area.
Last modified: Thu Sep 15 18:08:25 CEST 2011