1  Introduction

This document describes the use of the RISC ProgramExplorer, an interactive program reasoning environment which has been developed at the Research Institute for Symbolic Computation (RISC) and which integrates the previously developed RISC ProofNavigator [8, 5] as an interactive proving assistant. The environment allows to formally specify, analyze, and verify programs written in a subset of Java based on a calculus developed in [6, 7, 9]. In more detail,

• the RISC ProgramExplorer allows the user to elaborate mathematical theories and to formally specify a program on the basis of these theories;
• it translates the specified program into a semantic model which describes programs commands as state relations and which is open for human investigation;
• it generates from the semantic model the verification conditions which can be semi-automatically proved with the help of the RISC ProofNavigator.

The software provides an advanced graphical user interface that links theories, programs, semantic models, and verification tasks and allows the user to conveniently navigate between the different views.

The system is freely available under the GNU Public License at the URL

The software has been reasonably well tested but is certainly not free of bugs; the author is glad to receive error reports at

The remainder of the document is split in two parts:

• Chapters 2–4 essentially represent a tutorial for the RISC ProgramExplorer based on examples contained in the software distribution; for learning to use the system, we recommend to study this material in sequence.
• Appendices A–H essentially represent a reference manual with an explanation of the software’s programming and specification language; this material can be studied on demand.

This document does not explain in detail how to interactively prove the generated verification conditions; this is described in the manual of the RISC ProofNavigator [5].

The RISC ProgramExplorer uses the following third party software; detailed references can be found in the file of the distribution:

• CVC3
• CVC Lite
• RIACA OpenMath Library
• General Purpose Hash Function Algorithms Library
• ANTLR
• Eclipse Standard Widget Toolkit
• Mozilla Firefox
• GIMP Toolkit GTK+
• Sun JDK
• Tango Icon Library

Many thanks to the respective authors for their great work.