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)
Schedule
In Dagstuhl Seminar 24171, we brought together researchers working in various aspects of automated functional synthesis. This diverse topic encompasses areas ranging from Boolean variants to quantified variants, automated reasoning for general theories, program synthesis, and more. One particular focus was on finding synergies between functional and reactive synthesis communities and investigating the deep connections between these two areas.
setting the agenda for the entire seminar. This was succeeded by technical presentations on definability and dependency in quantified Boolean formulas. The second day included a tutorial on automated reasoning and synthesis, with an emphasis on theories extending beyond Boolean (e.g., SMT), followed by discussions on quantitative properties. On the third day, we organized a special session with other tool competition organizers to assess the feasibility of a competition or track dedicated to functional synthesis.
The remaining days were filled with diverse technical talks that fell into two categories. The first category included talks that delved deeper into specific aspects of functional synthesis, reactive/LTL synthesis, and specific problems within these fields. The second category introduced new applications or connections, such as quantum applications and functional programming. Discussions during and beyond these talks were further explored in different open and problem sessions. Some of the identified and discussed problems were:
- How to formalize the Boolean functional synthesis problem at the heart of reactive synthesis? Various problem formulations were discussed, and some benchmarks were created.
- Can we go beyond Boolean theories and synthesize programs and functions for general SMT? What bottlenecks do we face?
- How can we find synergy between automated functional synthesis and synthesis using transformers? Specifically, what is the meeting ground between machine learning and inductive program synthesis techniques, functional synthesis, and automated reasoning?
- Can the successful lens of knowledge representations and compilations for model counting and Boolean functional synthesis be extended to other settings?
- Can we synthesize quantum circuits from specifications, thus leading to a theory of automated reasoning for quantum systems?
- Can reactive synthesis over finite traces utilize techniques developed in automated functional synthesis?
These were among the prominent topics discussed, but the list is by no means exhaustive. Several bottlenecks were identified, such as the need for growth within the community developing these tools before establishing a proper competition. Additionally, there was a recognized necessity for broader and more extensive discussions on benchmarks.
Overall, the seminar fostered a collaborative spirit among theoreticians, tool developers, and experts across different aspects of automated functional synthesis. The seminar was also attended by a large number of early career researchers, postdoctoral fellows, and graduate students who also participated enthusiastically throughout the seminar. The shared optimism generated during this seminar has laid a strong foundation for future advancements. We advocate for the continuation of these valuable discussions and propose organizing further meetings of a similar nature to build on the momentum gained and to explore new frontiers in automated functional synthesis.
In the full report, we provide the abstracts of all the talks, as well as discussion sessions held during the seminar. We thank all the speakers and attendees for their active participation and look forward to attending and organizing more such events in the future.
Creative Commons BY 4.0
S. Akshay, Bernd Finkbeiner, Kuldeep S. Meel, and Ruzica Piskac
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.
S. Akshay, Bernd Finkbeiner, Kuldeep S. Meel, and Ruzica Piskac
- 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
