Alexander Kittelmann

Context: The laborious task of software specification is still hindering the practical application of deductive verification. The decision between method inlining and method contracting is an additional configuration option to increase the scalability of deductive verification. It can reduce or increase the specification effort and verification effort for software projects by abstracting method calls with their respective contracts. It is therefore reasonable to study prediction models for deciding automatically when to inline an implementation or when to use its contract.

Goal: We began to study this parameter in the verification system KeY with respect to provability, verification effort, and specification effort, but there are many questions left open. For instance, one goal could be to introduce a new keyword to JML to explicitly mark methods that should be either inlined or whose contract should be used. Another goal is to define a heuristic  (some form of statistical model) that may reason about which approach is more profitable for a given verification task. Additionally, part of the thesis is to identify important use cases for an optimal mix of inlining and method contracting (e.g., iterative development process and specification budget).

Prerequisites: Basic knowledge of Design-by-Contract; JML and Java (or a different specification language)