Topics for diploma theses, Master's theses and practical work

Themes for diploma theses, Master's theses and practical work arise predominantly in the realm of requirements engineering, software engineering, compiler construction and constraint programming. Our regularly offered courses communicate the necessary foundations. The topics are aligned to our research. Moreover, we are ready to discuss your own themes. If you are interested, please contact our lecturers.
The following, incomplete list states a range of concrete topics and domains. To receive further information, please contact the appropriate person.

• Bounded Reachability Analysis of Model Programs using BoogiePL as Intermediate Language
  Model programs are a subset of Abstract State Machines (http://www.eecs.umich.edu/gasm/). This formal language is used to specify and verify protocols or programs. For the verification, it is necessary to transform model programs into a verification condition. This logical formula is proven or rebutted by an (automatic) theorem prover.
  Within the scope of the Microsoft Research's project Spec# (http://research.microsoft.com/SpecSharp/) an intermediate language called BoogiePL was developed for program verification. This intermediate language offers higher level constructs than most of the current theorem prover. Now, the goal of this thesis is to translate model programs (or at least parts of them) via BoogiePL into a verification condition such that their correctness (for a bounded number of steps) can be proven.
  contact: Alexander Raschke
• A list of Thom Frühwirth's topics
  contact: Thom Frühwirth
• Various practicals and topics for theses in the area of constraint programming and Constraint Handling Rules are described here.