TOP
Suche auf der Schloss Dagstuhl Webseite
Sie suchen nach Informationen auf den Webseiten der einzelnen Seminare? - Dann:
Nicht fündig geworden? - Einige unserer Dienste laufen auf separaten Webseiten mit jeweils eigener Suche. Bitte beachten Sie folgende Liste:
Schloss Dagstuhl - LZI - Logo
Schloss Dagstuhl Services
Seminare
Innerhalb dieser Seite:
Externe Seiten:
  • DOOR (zum Registrieren eines Dagstuhl Aufenthaltes)
  • DOSA (zum Beantragen künftiger Dagstuhl Seminare oder Dagstuhl Perspektiven Workshops)
Publishing
Innerhalb dieser Seite:
Externe Seiten:
dblp
Innerhalb dieser Seite:
Externe Seiten:
  • die Informatik-Bibliographiedatenbank dblp


Dagstuhl-Seminar 24171

Automated Synthesis: Functional, Reactive and Beyond

( 21. Apr – 26. Apr, 2024 )

Permalink
Bitte benutzen Sie folgende Kurz-Url zum Verlinken dieser Seite: https://www.dagstuhl.de/24171

Organisatoren

Kontakt

Dagstuhl Seminar Wiki

Gemeinsame Dokumente

Programm
  • 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

Teilnehmer

Klassifikation
  • Artificial Intelligence
  • Logic in Computer Science

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