Tianhai Liu, Christoph Gladisch

The KeY verification system (developed at our institute) proves that a Java program satisfies its specification. The specification to be verified is provided by the user using a formal specification language. Currently, KeY only accepts specifications written in the Java Modeling Language (JML). JML is a behavioral specification language which integrates seamlessly into Java, adding first-order logic constructs to Java expressions. However, JML specifications tend to be close to the implementation and thus it is often difficult to formulate abstract concepts in it.

Alloy, on the other hand, is a lightweight formal language developed at MIT for formalising structurally complex systems. Its language is based on relational expressions which make it particularly suitable for expressing data-dependent systems succinctly.

The task of this thesis project is to investigate how Alloy can be used as the specification language of the KeY system. In this project, the specifications written in the Alloy language will be automatically translated to a subset of JML. Such a translation enables us to analyze Alloy specifications not only using KeY, but also using any other tool that supports JML. The translation/thesis will be guided by a few concrete examples.

Basic knowledge of first order logic, as for instance taught in the course "Formale Systeme" is required. Familiarity with Alloy and/or JML is preferred, but not necessary.

This thesis is a joint project between the groups Automatic Software Analysis (led by Mana Taghdiri), Logic and Formal Methods (led by Peter H. Schmitt), and Application-oriented Formal Verification (led by Bernhard Beckert).

If interested, please contact Mattias Ulbrich (ulbrich@kit.edu), Tianhai Liu (liu@ira.uka.de), or Christoph Gladisch (gladisch@ira.uka.de)