The RISC ProgramExplorer
December 7, 2020: RISC ProgramExplorer 2.27 (packaged with eclipse-2020-09 packages, fixed minor bugs)
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
|Click to run Flash screencast.
Click to enlarge screenshot.
Virtual Machine: You can download a pre-configured
virtual Linux machine
(for the free VirtualBox
with the RISC ProgramExplorer for execution under MS Windows, Mac OS, or Linux:
Virtual Machine with the
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
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.
module load ProgramExplorer
- Download the RISC
- This is a binary distribution for GNU/Linux x86 computers (32-bit or
See the files README, INSTALL,
- Tutorial and Manual [HTML | PDF]
- This is the user documentation for the software (see the
separate manual for the
on how to use the proving interface).
- 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:
- 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)
2.7.6b2 and 3.1.3 (local copy of V2,
local copy of V3)
- Eclipse Standard Widget Toolkit
4.8 (local copy for GNU/Linux x86
- WebKit 1.2.X or newer
- GIMP Toolkit GTK+ 2.X or 3.X
- Java Development Kit SE 8
- Tango Icon Library (local copy)
- Talks, Reports, Publications
- Collected information on the RISC ProgramExplorer.
Last modified: June 29, 2018