RISC JKU

The RISC ProgramExplorer

June 22, 2023: RISC ProgramExplorer 2.29 (bundled with eclipse-2023-06 packages, switch to Java 17)

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
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 (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
svn://svn.risc.jku.at/schreine/FM-RISC3
Talks, Reports, Publications
Collected information on the RISC ProgramExplorer.

Wolfgang Schreiner
Last modified: June 22, 2023