Dagstuhl-Seminar — Automated Synthesis: Functional, Reactive and Beyond

Automated synthesis of systems from specifications has been a longstanding goal of computer science. This problem has been studied by theoreticians and practitioners over decades as witnessed by an extensive and continued stream of articles related to synthesis in top-tier conferences in the field of formal methods. Despite a lot of recent progress, scalability in practical applications is still a concern. Recent advances in SAT/SMT solvers, decision tree learners, and other computational engines present an opportunity for a breakthrough in scalability. These advances have already led to powerful tools in the subarea of functional synthesis, which focuses on the synthesis of functions from relational specifications. However, much work is left to be done in order to translate these successes into scalable algorithms for more comprehensive synthesis problems, such as reactive synthesis, which aims at the automatic construction of circuits, embedded controllers, and other reactive software with complex temporal requirements. This Dagstuhl Seminar seeks to build on the recent momentum in these communities, and aims to bring together researchers in functional synthesis, reactive synthesis, and sister communities to chart the way forward. There are three broad objectives of the seminar.