Output-Sensitive Algorithms for Reactive Synthesis (OSARES)
The project is funded by the European Research Council for five years, from 2016 to 2021, as an ERC Consolidator Grant.
Distributed embedded systems have started to transform the role of computing technology in all sectors of our society. Applications include transport systems, building technology, energy management, health care, infrastructure, and environmental protection. These applications constitute a disruptive technology with the potential of vast savings in terms of energy, environmental pollution, and implementation costs. The flipside of these benefits is the potential for significant economical and possibly even life-threatening damage that could be caused if a distributed system fails to function as intended. Designing distributed systems that are safe, stable, and robust is difficult, because local design decisions may have global consequences, and many objectives can only be realized when multiple components cooperate.
Reactive synthesis has the potential to revolutionize the development of distributed embedded systems. From a given logical specification, the synthesis algorithm automatically constructs an implementation that is correct-by-design. This allows the developer to focus on “what” the system should do instead of “how” it should be done. Because synthesis analyzes objectives, not implementations, it can be applied at an early design stage, long before the system has been implemented. The goal of OSARES is to develop output-sensitive synthesis algorithms. In addition to optimal performance in the size of the specification, such algorithms also perform optimally in the size and structural complexity of the implementation. We aim for the principled analysis of the dependencies of different metrics on the complexity of the problem, as well as for improving the state of the art in practical synthesis. This entails work on both the theoretical level and on symbolic search algorithms, such as constraint solvers. We develop output-sensitive synthesis algorithms for the general classes of (control-dominated) discrete, real-time, and distributed reactive systems. Benchmarks for our new algorithms come from classic application areas like hardware synthesis, and from new and much more challenging application areas like distributed control and coordination, which are far beyond the reach of the currently available synthesis algorithms.
OSARES in the News
News reports about OSARES appeared in Saarbrücker Zeitung, c’t magazin für computer technik (pdf), and SR Aktueller Bericht (video starts at 11:30).
Currently there are several open PhD student positions and one open postdoc position. If you are interested, contact Bernd Finkbeiner. Candidates for PhD student positions should additionally submit an application to the Saarbrücken Graduate School of Computer Science (mention your interest in OSARES).
- Borzoo Bonakdarpour, Bernd Finkbeiner. Program Repair for Hyperproperties. ATVA 2019
- Jesko Hecking-Harbusch, Niklas Metzger. Efficient Trace Encodings of Bounded Synthesis for Asynchronous Distributed Systems. ATVA 2019.
- Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, Ernst-Rüdiger Olderog. Model Checking Data Flows in Concurrent Network Updates. ATVA 2019.
- Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah. Approximate Automata for Omega-regular Languages. ATVA 2019.
- Gideon Geier, Philippe Heim, Felix Klein, Bernd Finkbeiner. Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications. FMCAD 2019.
- Jan Baumeister, Bernd Finkbeiner, Maximilian Schwenger, Hazem Torfah. FPGA Stream-Monitoring of Real-time Properties. EMSOFT 2019.
- Raven Beutner, Bernd Finkbeiner, Jesko Hecking-Harbusch. Translating Asynchronous Games for Distributed Synthesis. CONCUR 2019.
- Bernd Finkbeiner, Felix Klein, Ruzica Piskac, Mark Santolucito. Synthesizing Functional Reactive Programs. Haskell 2019.
- Norine Coenen, Bernd Finkbeiner, Cesar Sanchez, Leander Tentrup. Verifying Hyperliveness. CAV 2019.
- Rayna Dimitrova, Bernd Finkbeiner, Hazem Torfah. Synthesizing Approximate Implementations for Unrealizable Specifications. CAV 2019.
- Bernd Finkbeiner, Felix Klein, Ruzica Piskac, Mark Santolucito. Temporal Stream Logic: Synthesis beyond the Bools. CAV 2019.
- Peter Faymonville, Bernd Finkbeiner, Malte Schledjewski, Maximilian Schwenger, Marvin Stenger, Leander Tentrup, Hazem Torfah. StreamLAB: Stream-based Monitoring of Cyber-physical Systems. CAV 2019.
- Leander Tentrup, Markus N. Rabe. Clausal Abstraction for DQBF. SAT 2019.
- Bernd Finkbeiner, Lennart Haas, Hazem Torfah. Canonical Representations of k-Safety Hyperproperties. CSF 2019.
- Norine Coenen, Bernd Finkbeiner, Christopher Hahn, and Jana Hofmann. The Hierarchy of Hyperlogics. LICS 2019.
- Christopher Hahn, Marvin Stenger, and Leander Tentrup. Constraint-based Monitoring of Hyperproperties. TACAS 2019.
- Bernd Finkbeiner, Felix Klein, and Carsten Gerstacker. Bounded Synthesis of Reactive Programs. ATVA 2018.
- Bernd Finkbeiner, Christopher Hahn, and Tobias Hans. MGHyper: Checking Satisfiability of HyperLTL formulas beyond the ∃*∀* Fragment. ATVA 2018.
- Jesko Hecking-Harbusch and Leander Tentrup. Solving QBF by Abstraction. GandALF 2018.
- Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, and Leander Tentrup. Synthesizing Reactive Systems from Hyperproperties. CAV 2018.
- Markus N. Rabe, Leander Tentrup, Cameron Rasmussen, and Sanjit A. Seshia. Understanding and Extending Incremental Determinization for 2QBF. CAV 2018.
- Bernd Finkbeiner, Christopher Hahn, and Hazem Torfah. Model Checking Quantitative Hyperproperties. CAV 2018.
- Swen Jacobs, Leander Tentrup, and Martin Zimmermann. Distributed Synthesis for Parameterized Temporal Logics. Information and Computation.
- Hadas Kress-Gazit and Hazem Torfah. The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems. CREST 2018.
- Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, and Leander Tentrup. RVHyper: A Runtime Verification Tool for Temporal Hyperproperties. TACAS 2018.
- Bernd Finkbeiner and Felix Klein. Reactive Synthesis: Towards Output-Sensitive Algorithms. IOS Press.
- Ruediger Ehlers and Bernd Finkbeiner. Symmetric Synthesis. FSTTCS 2017.
- Bernd Finkbeiner and Paul Gölz. Synthesis in Distributed Environments. FSTTCS 2017.
- Bernd Finkbeiner and Andrey Kupriyanov. Causality-based Model Checking. CREST 2017.
- Bernd Finkbeiner and Hazem Torfah. The Density of Linear-time Properties. ATVA 2017.
- Florian-Michael Adolf, Peter Faymonville, Bernd Finkbeiner, Sebastian Schirmer, and Christoph Torens. Stream Runtime Monitoring on UAS. RV 2017.
- Swen Jacobs, Nicolas Basset, Roderick Bloem, Romain Brenguier, Maximilien Colange, Peter Faymonville, Bernd Finkbeiner, Ayrat Khalimov, Felix Klein, Thibaud Michaud, Guillermo A. Perez, Jean-Francois Raskin, Ocan Sankur, and Leander Tentrup. The 4th Reactive Synthesis Competition (SYNTCOMP 2017): Benchmarks, Participants and Results. SYNT 2017.
- Bernd Finkbeiner, Manuel Gieseking, Jesko Hecking-Harbusch, and Ernst-Rüdiger Olderog. Symbolic vs. Bounded Synthesis for Petri Games. SYNT 2017.
- Peter Faymonville, Bernd Finkbeiner, and Leander Tentrup. BoSy: An Experimentation Framework for Bounded Synthesis. CAV 2017.
- Leander Tentrup. On Expansion and Resolution in CEGAR Based QBF Solving. CAV 2017.
- Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito. Vehicle Platooning Simulations with Functional Reactive Programming. SCAV.
- Pedro R. D’Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, and Holger Hermanns. Is your software on dope? ⋆ Formal analysis of surreptitiously “enhanced” programs. ESOP 2017.
- Peter Faymonville, Bernd Finkbeiner, Markus N. Rabe, and Leander Tentrup. Encodings of Bounded Synthesis. TACAS 2017.
- Bernd Finkbeiner. Synthesis of Reactive Systems. Verification and Synthesis of Correct and Secure Systems. Dependable Software Systems Engineering, 2016.
- Bernd Finkbeiner and Hazem Torfah. Synthesizing Skeletons for Reactive Systems. ATVA 2016.
- Gilles Barthe, Pedro R. D’Argenio, Bernd Finkbeiner, and Holger Hermanns. Facets of Software Doping. ISOLA 2016.
- Swen Jacobs, Leander Tentrup, and Martin Zimmermann. Distributed PROMPT-LTL Synthesis. GandALF 2016.
- Leander Tentrup, Alexander Weinert, and Martin Zimmermann. Approximating Optimal Bounds in Prompt-LTL Realizability in Doubly-exponential Time. GandALF 2016.
- Swen Jacobs, Roderick Bloem, Romain Brenguier, Ayrat Khalimov, Felix Klein, Robert Könighofer, Jens Kreber, Alexander Legg, Nina Narodytska, Guillermo A. Perez, Jean-Francois Raskin, Leonid Ryzhyk, Ocan Sankur, Martina Seidl, Leander Tentrup, and Adam Walker. The Third Reactive Synthesis Competition (SYNTCOMP 2016): Benchmarks, Participants and Results. SYNT 2016.
- Bernd Finkbeiner and Felix Klein. Bounded Cycle Synthesis. CAV 2016.