Maximilian Kodetzki

Context: Correctness-by-Construction (CbC) is an approach to construct functionally correct programs by applying correctness-preserving refinement rules. In difference to traditional software development techniques, CbC always starts with defining a formal specification describing the intended behavior. This leads to earlier feedback on the correctness of the constructed program as, for example, when using post-hoc verification techniques. In recent years, the approach of CbC was extended to consider non-functional properties, e.g., resource consumption, security, and reliability, besides its main aspect, functionality. In this context, prior work integrated energy consumption as property into by-Construction engineering which allows constructing functionally correct programs while ensuring that a certain energy bound is not exceeded.

Goal: The goal of this thesis is to apply the developed concepts for energy consumption in by-Construction engineering to the properties time and memory. Thereby, the energy concepts will serve as a basis which the new concepts shall be developed on. The thesis also includes the development of (prototypical) tool support.

Requirements: Students should have an idea what formal methods are, have basic skills in formal verification and logics. Lecture formal systems at KIT is of advantage. Motivation to work with formal topics is necessary.