PM Student Projects - Andreas Kaegi
The goal of this master's project is to develop a frontend that translates a JML-annotated
Java program into a set of input files for the Coq theorem prover. These generated files, specific
to every program, complement the syntax and semantics common to all programs with the concrete
program specification and implementation, as well as additional type and declaration information.
The Java and JML source is first translated into a Coq embedding that supports the full syntax of
JML. This embedding is then reduced into a form using only basic JML syntax, where all rewriteable
constructs have been replaced.
| Project Timeframe: |
September 2008 to March 2009 |
| Project Description: |
PDF |
| Supervisor: |
Hermann Lehner |
|
