Opendata, web and dolomites


Output-Sensitive Algorithms for Reactive Synthesis

Total Cost €


EC-Contrib. €






Project "OSARES" data sheet

The following table provides information about the project.


Organization address
address: CAMPUS
postcode: 66123

contact info
title: n.a.
name: n.a.
surname: n.a.
function: n.a.
email: n.a.
telephone: n.a.
fax: n.a.

 Coordinator Country Germany [DE]
 Project website
 Total cost 1˙995˙000 €
 EC max contribution 1˙995˙000 € (100%)
 Programme 1. H2020-EU.1.1. (EXCELLENT SCIENCE - European Research Council (ERC))
 Code Call ERC-2015-CoG
 Funding Scheme ERC-COG
 Starting year 2016
 Duration (year-month-day) from 2016-07-01   to  2021-06-30


Take a look of project's partnership.

# participants  country  role  EC contrib. [€] 


 Project objective

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. The vision is that a designer analyzes the design objectives with a synthesis tool, automatically identifies competing or contradictory requirements and obtains an error-free prototype implementation. Coding and testing, the most expensive stages of development, are eliminated from the development process. Recent case studies from robotic control and from hardware design, such as the automatic synthesis of the AMBA AHB bus controller, demonstrate that this vision is in principle feasible. So far, however, synthesis does not scale to large systems. Even if successful, it produces code that is much larger and much more complicated than the code produced by human programmers for the same specification. Our goal is to address both of these fundamental shortcomings at the same time. We will develop output-sensitive synthesis algorithms, i.e. algorithms that, in addition to optimal performance in the size of the specification, also perform optimally in the size and structural complexity of the implementation. Target applications for our algorithms come from both the classic areas of reactive synthesis, such as hardware circuits, and from new and much more challenging application areas such as the distributed control and coordination of autonomous vehicles and manufacturing robots, which are far beyond the reach of the currently available synthesis algorithms.


year authors and title journal last update
List of publications.
2019 Bernd Finkbeiner, Christopher Hahn, Marvin Stenger, Leander Tentrup
Monitoring hyperproperties
published pages: 336-363, ISSN: 0925-9856, DOI: 10.1007/s10703-019-00334-z
Formal Methods in System Design 54/3 2020-04-07
2019 Jacobs, Swen; Bloem, Roderick; Colange, Maximilien; Faymonville, Peter; Finkbeiner, Bernd; Khalimov, Ayrat; Klein, Felix; Luttenberger, Michael; Meyer, Philipp J.; Michaud, Thibaud; Sakr, Mouhammad; Sickert, Salomon; Tentrup, Leander; Walker, Adam
The 5th Reactive Synthesis Competition (SYNTCOMP 2018): Benchmarks, Participants & Results
published pages: , ISSN: 2331-8422, DOI:
arXiv preprint arXiv:1904.07736 2020-04-07
2020 Bernd Finkbeiner, Christopher Hahn, Philip Lukert, Marvin Stenger, Leander Tentrup
Synthesis from hyperproperties
published pages: 137-163, ISSN: 0001-5903, DOI: 10.1007/s00236-019-00358-2
Acta Informatica 57/1-2 2020-04-07
2019 Jan Baumeister, Bernd Finkbeiner, Maximilian Schwenger, Hazem Torfah
FPGA Stream-Monitoring of Real-time Properties
published pages: 1-24, ISSN: 1539-9087, DOI: 10.1145/3358220
ACM Transactions on Embedded Computing Systems 18/5s 2020-04-07
2017 Peter Faymonville, Bernd Finkbeiner, Maximilian Schwenger, Hazem Torfah
Real-time Stream-based Monitoring
published pages: , ISSN: 2331-8422, DOI:
arXiv preprint arXiv:1711.03829 2019-06-06
2017 Bernd Finkbeiner, Felix Klein, Ruzica Piskac, Mark Santolucito
Synthesizing Functional Reactive Programs
published pages: , ISSN: 2331-8422, DOI:
arXiv preprint arXiv:1712.00246 2019-06-06
2019 Hadas Kress-Gazit, Hazem Torfah
The Challenges in Specifying and Explaining Synthesized Implementations of Reactive Systems
published pages: 50-64, ISSN: 2075-2180, DOI: 10.4204/eptcs.286.5
Electronic Proceedings in Theoretical Computer Science 286 2019-05-22
2016 Swen Jacobs, Felix Klein, Sebastian Schirmer
A High-Level LTL Synthesis Format: TLSF v1.1
published pages: 112-132, ISSN: 2075-2180, DOI: 10.4204/eptcs.229.10
Electronic Proceedings in Theoretical Computer Science 229 2019-05-22
2018 Swen Jacobs, Leander Tentrup, Martin Zimmermann
Distributed synthesis for parameterized temporal logics
published pages: 311-328, ISSN: 0890-5401, DOI: 10.1016/j.ic.2018.09.009
Information and Computation 262 2019-05-22
2018 Jesko Hecking-Harbusch, Leander Tentrup
Solving QBF by Abstraction
published pages: 88-102, ISSN: 2075-2180, DOI: 10.4204/eptcs.277.7
Electronic Proceedings in Theoretical Computer Science 277 2019-05-22

Are you the coordinator (or a participant) of this project? Plaese send me more information about the "OSARES" project.

For instance: the website url (it has not provided by EU-opendata yet), the logo, a more detailed description of the project (in plain text as a rtf file or a word file), some pictures (as picture files, not embedded into any word file), twitter account, linkedin page, etc.

Send me an  email ( and I put them in your project's page as son as possible.

Thanks. And then put a link of this page into your project's website.

The information about "OSARES" are provided by the European Opendata Portal: CORDIS opendata.

More projects from the same programme (H2020-EU.1.1.)

BABE (2018)

Why is the world green: testing top-down control of plant-herbivore food webs by experiments with birds, bats and ants

Read More  


Exploiting genome replication to design improved plant growth strategies

Read More  

AST (2019)

Automatic System Testing

Read More