The RISC ProgramExplorer: Reasoning about Programs as State Relations (Extended Abstract)

We report on the formal framework underlying the RISC ProgramExplorer, a program reasoning environment which is under development at the Research Institute for Symbolic Computation (RISC) and which integrates the previously developed RISC ProofNavigator as an interactive proving assistant. The current release of the software is a first demonstrator that incorporates the overall technological framework (including an elaborated graphical user interface) and language processors (for a simple subset of Java as a programming language and a formal specification language). Work is going on to provide this skeleton with the envisioned program reasoning capabilities. The goal of this presentation is to outline the formal basis underlying these capabilities and to explain the rationale for its particular design.