Wolfgang Schreiner,
"The RISC ProgramExplorer - Tutorial and Manual"
, Nummer 11-11, RISC JKU, Hagenberg, 10-2011
Original Titel:
The RISC ProgramExplorer - Tutorial and Manual
Sprache des Titels:
Englisch
Original Kurzfassung:
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.
Forschungs-