The RISC ProgramExplorer: Tutorial and Manual

This document describes the use of the RISC ProgramExplorer, an interactive program reasoning environment that is under development at the Research Institute for Symbolic Computation (RISC). The current version is a first demonstrator skeleton that incorporates the overall technological and semantic framework (programming language and formal specification language) and integrates the RISC ProofNavigator as an interactive proving assistant. Work is going on to provide this skeleton with the envisioned program reasoning capabilities. 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.