TOP
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
Seminars
Within this website:
External resources:
  • DOOR (for registering your stay at Dagstuhl)
  • DOSA (for proposing future Dagstuhl Seminars or Dagstuhl Perspectives Workshops)
Publishing
Within this website:
External resources:
dblp
Within this website:
External resources:
  • the dblp Computer Science Bibliography


Dagstuhl Seminar 24171

Automated Synthesis: Functional, Reactive and Beyond

( Apr 21 – Apr 26, 2024 )

Permalink
Please use the following short url to reference this page: https://www.dagstuhl.de/24171

Organizers

Contact

Dagstuhl Seminar Wiki

Shared Documents

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

Motivation

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

Participants

Classification
  • Artificial Intelligence
  • Logic in Computer Science

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