Search the Dagstuhl Website
Looking for information on the websites of the individual seminars? - Then please:
Not found what you are looking for? - Some of our services have separate websites, each with its own search option. Please check the following list:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Within this website:
External resources:
Within this website:
External resources:
  • the dblp Computer Science Bibliography

Dagstuhl Seminar 24171

Automated Synthesis: Functional, Reactive and Beyond

( Apr 21 – Apr 26, 2024 )

(Click in the middle of the image to enlarge)

Please use the following short url to reference this page:



Dagstuhl Reports

As part of the mandatory documentation, participants are asked to submit their talk abstracts, working group results, etc. for publication in our series Dagstuhl Reports via the Dagstuhl Reports Submission System.

  • Upload (Use personal credentials as created in DOOR to log in)

Dagstuhl Seminar Wiki

Shared Documents



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.

The first objective is to enable discovery of synergy across a diverse array of complementary approaches to functional synthesis. These approaches include (i) Knowledge Compilation-Based Approaches motivated by the success of such approaches in Bayesian inference; (ii) Guess-Check-Repair approaches that involve an intelligent initial guess of the desired system, followed by using an efficient solver to check if the guess satisfies the user’s requirements and incrementally repairs the system if it does not; (iii) Data-Driven Synthesis approaches that focus on utilizing recent advances in constrained sampling to generate data (or examples), which is then fed to machine learning techniques to generate initial candidate functions, which are then repaired, (iv) Incremental Determinization approaches that are motivated by the success of conflict-driven clause learning (CDCL) techniques in the context of search for satisfying assignments for Boolean formulas.

The second objective of this seminar is to enable the community to chart the way forward via standardization of tools and foster a competitive event for tools. To this end, we expect the seminar to provide an avenue for the community to discuss different proposals regarding standardization of interfaces, benchmark selection, evaluation mechanisms and validation of results.

Finally, the field of automated reasoning has witnessed significant progress whenever a virtuous cycle between foundational advances and practical applications is attained. The third objective of the seminar is to explore whether such a virtuous cycle can be established in the context of functional and reactive synthesis. Beyond this, the seminar will also discuss the relationships and challenges when considering other (possibly orthogonal) extensions, e.g., functional synthesis for more general first-order logic specifications, synthesis for hybrid systems and program synthesis.

Copyright S. Akshay, Bernd Finkbeiner, Kuldeep S. Meel, and Ruzica Piskac


  • Artificial Intelligence
  • Logic in Computer Science

  • Automated synthesis
  • Boolean functions
  • knowledge representations
  • reactive synthesis
  • SAT/SMT solvers