Tabea Bordis

Context: Correctness-by-Construction (CbC) is a method for software development. Here programs are provided with formal specifications and created by correctness-preserving refinements. The CorC tool provides the ability to develop programs using CbC. Program synthesis is about automatically synthesizing programs that meet the specification from a formal specification, as is also used in CbC.

Aim: In the master's thesis, program synthesis techniques will be introduced and a concept will be developed to apply them to CbC as implemented in the tool CorC. The thesis will also evaluate the degree to which program synthesis can be implemented with the resulting concept and how well the synthesized programs fit their specifications.

Prerequisite: Programming knowledge in Java, basic knowledge in the area of program verification and specification.