RISC-Linz RISC-Linz Research Institute for Symbolic Computation  
description  |  members  |  activities  |  seminar  |  publications  |  software

The RISC ProgramExplorer

June 23, 2016: RISC ProgramExplorer 2.16 (packaged with SWT 4.6)

The RISC ProgramExplorer is a computer-supported program reasoning environment for a simple imperative programming language "MiniJava"; it incorporates the RISC ProofNavigator as a semi-automatic proving assistant. The environment has been developed mainly for educational purposes (see this paper for a sketch of the main ideas). 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 to run Flash screencast. Click to enlarge screenshot.

Virtual Machine: You can download a pre-configured virtual Linux machine (for the free VirtualBox virtualization software) with the RISC ProgramExplorer for execution under MS Windows, Mac OS, or Linux:
Virtual Machine with the RISC ProgramExplorer
To start the software, login as user "guest" with password "guest", double-click the "Terminal" icon, then execute "cd examples-ProgramExplorer-CVC3" and "ProgramExplorer &". As a small demo, double-click the class "Factorial" in the left panel, then right-click the method "fac" and select "Show Semantics" to investigate the semantics of the method as a relation on program states.
RISC Users: The RISC ProgramExplorer is installed in the RISC environment. To start the software (respectively the included new version of the RISC ProofNavigator), execute
module load ProgramExplorer
ProgramExplorer &
(ProofNavigator &)
Download the RISC ProgramExplorer 2.16
This is a binary distribution for GNU/Linux x86 computers (32-bit or 64-bit).
Tutorial and Manual [HTML | PDF]
This is the user documentation for the software (see the separate manual for the RISC ProofNavigator on how to use the proving interface).
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
Third Party Software
The following third-party software is used by the ProofNavigator:
CVC3 (local copy of version 2.4.1)
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 and 3.1.3 (local copy of V2, local copy of V3)
Eclipse Standard Widget Toolkit 4.6 (local copy for GNU/Linux x86 32 bit and 64 bit)
XULRunner 24.0 (README, local copy for GNU/Linux x86 32 bit and 64 bit)
GIMP Toolkit GTK+ 2.X
Java Development Kit SE 8
Tango Icon Library (local copy)
Talks, Reports, Publications
Collected information on the RISC ProgramExplorer.

Wolfgang Schreiner
Last modified: July 13, 2015