The RISC ProgramExplorer - Tutorial and Manual

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 as an interactive proving assistant. The environment allows to formally specify, analyze, and verify programs written in a subset of Java. For this purpose, it translates annotated programs into a semantic model which describes programs as state relations and is open for human investigation; from this model the software generates verification conditions which can be semi-automatically proved. Within the environment the user may elaborate mathematical theories as the basis of program specifications; an advanced graphical user interface links theories, programs, semantic models, and verification tasks and allows to easily navigate between the different views.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.