Master's Thesis

The goal of this project is to formalize a basic imperative language with pointers and arrays, and provide a proof infrastructure (e.g. Separation Logic) and/or a translation to a real imperative language (e.g. Java, C).

Isabelle/HOL is a theorem prover based on higher-order logic. It is particularly suited to formalize the semantics of programming languages. In this thesis, the semantics of a simple C-like language shall be formalized. The language shall be expressive enough to allow for efficient implementations of basic algorithms (e.g. sorting, depth-first search) but at the same time as simple as possible to allow for a concise semantics.

Tasks:
Once the semantics is established, this project can go in several directions:
  • Formalize proof rules for the language. To reason with pointers, a separation logic will be needed.
  • Write a code-generator that emits Java or C code.
  • Link the language with the Isabelle Refinement Framework, such that programs from the Isabelle Refinement Framework can be refined to programs in this language.
Prerequisites:
Experience with Isabelle/HOL (e.g. the Course "Interactive Software Verification" or "Semantics") Knowledge of an imperative programming language, e.g. C or Java.
Related:
The Material of the course "Interactive Software Verification" contains a related approach, where a simple fragment of C is parsed into Isabelle and verified (bottom-up approach). In contrast, this project is targeted towards a top-down approach.
Advisor:
Peter Lammich, Raum MI 00.09.065, email {lammich} AT [in.tum.de]
Supervisor:
Prof. Tobias Nipkow, Raum MI 00.09.055, email {nipkow} AT [in.tum.de]