Abstract
This paper covers the Rigorous Examination of Reactive Systems (RERS) Challenge 2019. For the first time in the history of RERS, the challenge features industrial tracks where benchmark programs that participants need to analyze are synthesized from real-world models. These new tracks comprise LTL, CTL, and Reachability properties. In addition, we have further improved our benchmark generation infrastructure for parallel programs towards a full automation. RERS 2019 is part of TOOLympics, an event that hosts several popular challenges and competitions. In this paper, we highlight the newly added industrial tracks and our changes in response to the discussions at and results of the last RERS Challenge in Cyprus.
Original language | English |
---|---|
Title of host publication | Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of TACAS |
Subtitle of host publication | TOOLympics, Held as Part of ETAPS 2019, Proceedings |
Editors | Bernhard Steffen, Dirk Beyer, Fabrice Kordon, Marieke Huisman |
Place of Publication | Cham |
Publisher | Springer |
Pages | 101-115 |
Number of pages | 15 |
ISBN (Electronic) | 978-3-030-17502-3 |
ISBN (Print) | 978-3-030-17501-6 |
DOIs | |
Publication status | Published - 2019 |
Event | 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019 - Prague, Czech Republic Duration: 6 Apr 2019 → 11 Apr 2019 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 11429 LNCS |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019 |
---|---|
Country/Territory | Czech Republic |
City | Prague |
Period | 6/04/19 → 11/04/19 |
Funding
Acknowledgments. This work was partially performed under the auspices of the U.S. Department of Energy by Lawrence Livermore National Laboratory under Contract DE-AC52-07NA27344, and was supported by the LLNL-LDRD Program under Project No. 17-ERD-023. IM Release Nr. LLNL-CONF-766478.
Keywords
- Benchmark generation
- CTL
- LTL
- Obfuscation
- Program verification
- Property-preservation
- Synthesis
- Temporal logics