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.
| Original language | English |
|---|---|
| Title of host publication | SCSS 2010 |
| Editors | Mohamed Mosbah and Tudor Jebelean |
| Number of pages | 13 |
| Publication status | Published - 2010 |
Fields of science
- 101001 Algebra
- 101002 Analysis
- 101 Mathematics
- 102 Computer Sciences
- 102011 Formal languages
- 101013 Mathematical logic
- 101020 Technical mathematics
- 101025 Number theory
- 101012 Combinatorics
- 101005 Computer algebra
- 101003 Applied geometry
- 102025 Distributed systems
JKU Focus areas
- Computation in Informatics and Mathematics
- Engineering and Natural Sciences (in general)