Working Group 4 on Synthesis

Topics of Interest: New algorithms for synthesis from high-level specifications. Extending decision procedures to perform synthesis tasks. Connections between invariant generation and code synthesis.

Working Group 4 explores the theory, tools, and usability of synthesis in system development. In contrast to automated verification algorithms, which establish whether a given system satisfies a given specification, synthesis algorithms automatically construct implementation that is guaranteed to satisfy a given specification. Synthesis is more difficult than verification, and is one of the holy grails of Computer Science. Despite impressive theoretical results of the past, it was only recently that researchers made significant steps towards the development of practical synthesis algorithms. Synthesis still has many limitations preventing its wider practical application. Working Group 4 aims to address these limitations through tasks that include the following. * Developing synthesis algorithms for more expressive logics, including identifying decidability and worst-case complexity of synthesis for expressive logics, developing heuristics and new subclasses of problems that overcome high complexity, lifting decision problems (explored in Working Group 2) to synthesis problems, developing high-level synthesis techniques applicable to components, and synthesis of hybrid systems.

  • Efficient implementations of synthesis algorithms using not only binary decision diagrams but also quantified (Boolean) formulas, and the development of benchmarks for synthesis problems within the Rich Model benchmark suite from Working Group 1.
  • Quantitative generalization of synthesis, including: extending Boolean specifications by quantitative measures in order to rank implementations by laziness, fairness, or parsimonious use of resources, non-Boolean algorithms that generalize decision procedures from Working Group 2, and quantitative games as a method for solving synthesis problems.
  • Simplified synthesis problems of practical interest, including problems with limited quantifier alternations, using synthesis for problems where some part of the structure is predefined (e.g., repair, sketching).
  • Using synthesis to implement high-level programming language constructs.

Action experts have a unique set of complementary skills, whose combination will be necessary to fulfill the research vision of synthesis. By giving a more active role to automated tasks and avoiding low-level coding, synthesis has the potential to dramatically improve the productivity of computer system developers.

Research on Synthesis within and outside of the action

Below we give an incomplete list of pointers to research within and outside the action related to this working group. This is list under construction. Feel free to extend it.

Synthesizers from Linear Temporal Logic (LTL or LTL-like) Specifications

Here is an incomplete list of people and tools on the topic of synthesis from linear temporal logic specifications.

Notes on a common format for LTL synthesis.

Other Game Solvers

  • NuGat (FBK Trento)
  • GAVS+ (TUM, Fortiss)
  • GIST (IST Austria, Verimag Grenoble)
  • pgsolver (LMU, University of Kassel)
  • UPPAL-TIGA Solver for timed games
  • GasT (RWTH Aachen) not maintained anymore

Synthesizers for Sequential Code, Code-Snippets, or Synchronization