Program Synthesis

Making changes to code automatically

Every programmer spends a lot of time writing code that they find straightforward. This includes fixing simple bugs, or finishing an implementation of yet another recursive method. In today’s tools, these need to be done completely manually, or at best, providing a pre-defined list of patterns through an IDE that can be used, to save programmer some typing.

Using our research results allows us to replace syntactic patterns with analysing the actual semantics of the code. This gives us an ability to apply refactoring in many more contexts. We also use our approach in error repair, to find changes of the programs that eliminate detected bugs while not changing any other behaviour. Techniques we use for program synthesis include genetic algorithms, and use of mathematical solvers.

Read our published work

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants by Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas Cordeiro, Cristina David, Pascal Kesseli, and Daniel Kroening

Modern control is implemented with digital microcontrollers, which are designed to work in an embedded environment, within a dynamical plant that represents physical components. We present a new algorithm based on counterexample guided inductive synthesis that automates the design of digital controllers that are correct by construction. The synthesis result is sound with respect to the complete range of approximations, including time discretization, quantization effects, and finite-precision arithmetic and their related rounding errors. We have implemented our new algorithm in a tool called DSSynth, and are able to automatically generate stable controllers for a set of intricate plant models taken from the literature within minutes.

Using Program Synthesis for Program Analysis by Cristina David, Daniel Kroening, and Matt Lewis

In this paper, we identify a fragment of second-order logic with restricted quantification that is expressive enough to capture numerous static analysis problems (e.g. safety proving, bug finding, termination and non-termination proving, superoptimisation). We call this fragment the {\it synthesis fragment}. Satisfiability of a formula in the synthesis fragment is decidable over finite domains; specifically the decision problem is NEXPTIME-complete. If a formula in this fragment is satisfiable, a solution consists of a satisfying assignment from the second order variables to \emph{functions over finite domains}. To concretely find these solutions, we synthesise \emph{programs} that compute the functions. Our program synthesis algorithm is complete for finite state programs, i.e. every \emph{function} over finite domains is computed by some \emph{program} that we can synthesise. We can therefore use our synthesiser as a decision procedure for the synthesis fragment of second-order logic, which in turn allows us to use it as a powerful backend for many program analysis tasks. To show the tractability of our approach, we evaluate the program synthesiser on several static analysis problems.

Permissive Controller Synthesis for Probabilistic Systems by Klaus Draeger, Vojtech Forejt, Marta Z. Kwiatkowska, David Parker, and Mateusz Ujma

We propose novel controller synthesis techniques for probabilistic systems modelled using stochastic two-player games: one player acts as a controller, the second represents its environment, and probability is used to capture uncertainty arising due to, for example, unreliable sensors or faulty system components. Our aim is to generate robust controllers that are resilient to unexpected system changes at runtime, and flexible enough to be adapted if additional constraints need to be imposed. We develop a permissive controller synthesis framework, which generates multi-strategies for the controller, offering a choice of control actions to take at each time step. We formalise the notion of permissivity using penalties, which are incurred each time a possible control action is disallowed by a multi-strategy. Permissive controller synthesis aims to generate a multi-strategy that minimises these penalties, whilst guaranteeing the satisfaction of a specified system property. We establish several key results about the optimality of multi-strategies and the complexity of synthesising them. Then, we develop methods to perform permissive controller synthesis using mixed integer linear programming and illustrate their effectiveness on a selection of case studies.

Observer-based correct-by-design controller synthesis by Sofie Haesaert, Paul M. J. Van den Hof, Alessandro Abate

Current state-of-the-art correct-by-design controllers are designed for full-state measurable systems. This work first extends the applicability of correct-by-design controllers to partially observable LTI systems. Leveraging 2nd order bounds we give a design method that has a quantifiable robustness to probabilistic disturbances on state transitions and on output measurements. In a case study from smart buildings we evaluate the new output-based correct-by-design controller on a physical system with limited sensor information.