The RISC ProgramExplorer
July 9, 2024: RISC ProgramExplorer 2.30 (bundled with eclipse-2024-06 packages)
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: July 9, 2024
