Dagstuhl Seminar 24171
Automated Synthesis: Functional, Reactive and Beyond
( Apr 21 – Apr 26, 2024 )
(Click in the middle of the image to enlarge)
Permalink
Please use the following short url to reference this page:
https://www.dagstuhl.de/24171
Organizers
- S. Akshay (Indian Institute of Technology Bombay - Mumbai, IN)
- Bernd Finkbeiner (CISPA - Saarbrücken, DE)
- Kuldeep S. Meel (University of Toronto, CA)
- Ruzica Piskac (Yale University - New Haven, US)
Contact
- Michael Gerke (for scientific matters)
- Simone Schilke (for administrative matters)
Shared Documents
- Dagstuhl Materials Page (Use personal credentials as created in DOOR to log in)
Schedule
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.
Creative Commons BY 4.0
S. Akshay, Bernd Finkbeiner, Kuldeep S. Meel, and Ruzica Piskac
Please log in to DOOR to see more details.
- S. Akshay (Indian Institute of Technology Bombay - Mumbai, IN) [dblp]
- Ashwani Anand (MPI-SWS - Kaiserslautern, DE)
- A. R. Balasubramanian (MPI-SWS - Kaiserslautern, DE) [dblp]
- Suguman Bansal (Georgia Institute of Technology - Atlanta, US) [dblp]
- Katrine Bjorner (New York University, US)
- José Cambronero (Microsoft - Redmond, US)
- Supratik Chakraborty (Indian Institute of Technology Bombay - Mumbai, IN) [dblp]
- Deepak D'Souza (Indian Institute of Science - Bangalore, IN) [dblp]
- Alexis de Colnet (TU Wien, AT)
- Rayna Dimitrova (CISPA - Saarbrücken, DE) [dblp]
- Rüdiger Ehlers (TU Clausthal, DE) [dblp]
- Johannes Klaus Fichte (Linköping University, SE)
- Bernd Finkbeiner (CISPA - Saarbrücken, DE) [dblp]
- Dror Fried (The Open University of Israel - Ra'anana, IL) [dblp]
- Mikoláš Janota (Czech Technical University - Prague, CZ) [dblp]
- Jie-Hong Roland Jiang (National Taiwan University - Taipei, TW)
- Ayrat Khalimov (TU Clausthal, DE) [dblp]
- Alfons Laarman (Leiden University, NL)
- Benedikt Maderbacher (TU Graz, AT)
- Pierre Marquis (University of Artois/CNRS - Lens, FR) [dblp]
- Kuldeep S. Meel (University of Toronto, CA) [dblp]
- Tobias Meggendorfer (Lancaster University Leipzig, DE)
- Jingyi Mei (Leiden University, NL)
- Guillermo A. Pérez (University of Antwerp, BE) [dblp]
- Ruzica Piskac (Yale University - New Haven, US) [dblp]
- Govind Rajanbabu (Indian Institute of Technology Bombay - Mumbai, IN)
- Subhajit Roy (Indian Institute of Technology Kanpur, IN) [dblp]
- Mark Santolucito (Barnard College, Columbia University - New York, US) [dblp]
- Ute Schmid (Universität Bamberg, DE) [dblp]
- Sanjit A. Seshia (University of California - Berkeley, US) [dblp]
- Shetal Shah (Indian Institute of Technology Bombay - Mumbai, IN)
- Arijit Shaw (Chennai Mathematical Institute, IN & University of Toronto, CA)
- Friedrich Slivovsky (University of Liverpool, GB) [dblp]
- Mate Soos (University of Toronto, CA) [dblp]
- K. S. Thejaswini (IST Austria - Klosterneuburg, AT) [dblp]
- Hazem Torfah (Chalmers University of Technology - Göteborg, SE) [dblp]
- Shufang Zhu (University of Oxford, GB)
Classification
- Artificial Intelligence
- Logic in Computer Science
Keywords
- Automated synthesis
- Boolean functions
- knowledge representations
- reactive synthesis
- SAT/SMT solvers
