In a nutshell

This thesis will investigate and develop techniques for the synthesis of reactive, concurrent programs.

Background & motivation

Program synthesis allows to automatically construct an operational program from a declarative specification of the program’s intent. The synthesis of general-purpose full-scale programs from abstract specifications of user intent, however, is currently out of reach. One way to address this general dilemma is not to try to synthesize full programs from scratch, but filling in gaps or missing pieces in partially given programs. Examples of successful such approaches in that direction are known as “sketching” or synthesis from “templates”, among others.

An interesting area is the synthesis of correct concurrent programs. The interest comes from the fact that correct programs under the assumption of sequential execution are, in comparison, more easy to achieve. Secondly, getting the synchronization correct (avoiding deadlocks, races and similar problems) is seen as much harder. Thus, the thesis investigates and devlops techniques to synthesize correct synchronization (and other aspects) in connection with concurrent programs. One potential general area of application are IoT system which are characterized by restricted amount of resources (memory, battery…).

Tasks

Concretely. the project will address the following tasks:

  • Give a state-of-the-art overview concerning synthesis of programs, especially in regards to concurrency and synchronization,
  • Investigate ways to leverage data from past invocations of the syntheziser by the “user” to help guide the search.
  • Investigate the opportunities for improving the synthesis with assistance of machine learning or evolutionary learning.
  • Implement the synthesis.
  • Evaluate the validitiy of the apporach and the implementation.