{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,19]],"date-time":"2026-05-19T01:04:49Z","timestamp":1779152689073,"version":"3.51.4"},"reference-count":72,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2021,6,24]],"date-time":"2021-06-24T00:00:00Z","timestamp":1624492800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,6,24]],"date-time":"2021-06-24T00:00:00Z","timestamp":1624492800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100016378","name":"Technische Universit\u00e4t Dortmund","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100016378","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2021,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper (1) summarizes the history of the RERS challenge for the analysis and verification of reactive systems, its profile and intentions, its relation to other competitions, and, in particular, its evolution due to the feedback of participants, and (2) presents the most recent development concerning the synthesis of hard benchmark problems. In particular, the second part proposes a way to tailor benchmarks according to the depths to which programs have to be investigated in order to find all errors. This gives benchmark designers a method to challenge contributors that try to perform well by excessive guessing.<\/jats:p>","DOI":"10.1007\/s10009-021-00617-z","type":"journal-article","created":{"date-parts":[[2021,6,24]],"date-time":"2021-06-24T12:02:40Z","timestamp":1624536160000},"page":"917-930","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["The RERS challenge: towards controllable and scalable benchmark synthesis"],"prefix":"10.1007","volume":"23","author":[{"given":"Falk","family":"Howar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Jasper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Malte","family":"Mues","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Schmidt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2021,6,24]]},"reference":[{"key":"617_CR1","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-319-03077-7_18","volume-title":"Hardware and Software: Verification and Testing","author":"S Apel","year":"2013","unstructured":"Apel, S., Beyer, D., Friedberger, K., Raimondi, F., von Rhein, A.: Domain types: abstract-domain selection based on variable usage. In: Bertacco, V., Legay, A. (eds.) Hardware and Software: Verification and Testing, pp. 262\u2013278. Springer, Cham (2013)"},{"key":"617_CR2","doi-asserted-by":"publisher","unstructured":"Apt, K.R., Olderog, E.R.: Verification of Sequential and Concurrent Programs. Texts and Monographs in Computer Science. Springer (1991). https:\/\/doi.org\/10.1007\/978-1-4757-4376-0","DOI":"10.1007\/978-1-4757-4376-0"},{"key":"617_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P., Larsen, K.G.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"617_CR4","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/11513988_4","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2005","unstructured":"Barrett, C., de Moura, L., Stump, A.: Smt-comp: satisfiability modulo theories competition. In: Etessami, K., Rajamani, S.K. (eds.) Computer Aided Verification, pp. 20\u201323. Springer, Berlin (2005)"},{"key":"617_CR5","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-17502-3_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E Bartocci","year":"2019","unstructured":"Bartocci, E., Beyer, D., Black, P.E., Fedyukovich, G., Garavel, H., Hartmanns, A., Huisman, M., Kordon, F., Nagele, J., Sighireanu, M., Steffen, B., Suda, M., Sutcliffe, G., Weber, T., Yamada, A.: Toolympics 2019: an overview of competitions in formal methods. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 3\u201324. Springer, Cham (2019)"},{"key":"617_CR6","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Falcone, Y., Bonakdarpour, B., Colombo, C., Decker, N., Havelund, K., Joshi, Y., Klaedtke, F., Milewicz, R., Reger, G., et\u00a0al.: First International Competition on Runtime Verification: Rules, Benchmarks, Tools, and Final Results of CRV 2014. STTT pp. 1\u201340 (2017)","DOI":"10.1007\/s10009-017-0454-5"},{"issue":"5","key":"617_CR7","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/s10009-014-0333-2","volume":"16","author":"O Bauer","year":"2014","unstructured":"Bauer, O., Geske, M., Isberner, M.: Analyzing program behavior through active automata learning. Int. J. Softw. Tools Technol. Transf. 16(5), 531\u2013542 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"617_CR8","series-title":"LNCS","first-page":"504","volume-title":"TACAS","author":"D Beyer","year":"2012","unstructured":"Beyer, D.: Competition on software verification. TACAS. LNCS, vol. 7214, pp. 504\u2013524. Springer, Berlin (2012)"},{"key":"617_CR9","doi-asserted-by":"publisher","unstructured":"Beyer, D.: Status Report on Software Verification. In: Proceedings of the TACAS, LNCS\u00a08413, pp. 373\u2013388. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_25","DOI":"10.1007\/978-3-642-54862-8_25"},{"key":"617_CR10","first-page":"1","volume-title":"Mathematical and Engineering Methods in Computer Science","author":"D Beyer","year":"2013","unstructured":"Beyer, D., Stahlbauer, A.: Bdd-based software model checking with cpachecker. In: Ku\u010dera, A., Henzinger, T.A., Ne\u0161et\u0159il, J., Vojnar, T., Anto\u0161, D. (eds.) Mathematical and Engineering Methods in Computer Science, pp. 1\u201311. Springer, Berlin (2013)"},{"issue":"5","key":"617_CR11","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/s10009-014-0334-1","volume":"16","author":"D Beyer","year":"2014","unstructured":"Beyer, D., Stahlbauer, A.: BDD-based software verification. Applications to event-condition-action systems. Int. J. Softw. Tools Technol. Transf. 16(5), 507\u2013518 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"617_CR12","doi-asserted-by":"publisher","unstructured":"Briggs, P., Cooper, K.D.: Effective partial redundancy elimination. In: Proceedings of the ACM SIGPLAN\u201994 Conference on Programming Language Design and Implementation (PLDI), pp. 159\u2013170 (1994). https:\/\/doi.org\/10.1145\/773473.178257","DOI":"10.1145\/773473.178257"},{"key":"617_CR13","doi-asserted-by":"publisher","unstructured":"B\u00fcchi, J.R.: Symposium on decision problems: On a decision method in restricted second order arithmetic. In: Logic, Methodology and Philosophy of Science, Studies in Logic and the Foundations of Mathematics, vol.\u00a044, pp. 1 \u2013 11. Elsevier (1966). https:\/\/doi.org\/10.1016\/S0049-237X(09)70564-6","DOI":"10.1016\/S0049-237X(09)70564-6"},{"key":"617_CR14","volume-title":"Model Checking","author":"EM Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"617_CR15","doi-asserted-by":"publisher","first-page":"513","DOI":"10.1007\/978-3-030-11245-5_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N Decker","year":"2019","unstructured":"Decker, N., Pirogov, A.: Flat model checking for counting ltl using quantifier-free presburger arithmetic. In: Enea, C., Piskac, R. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 513\u2013534. Springer, Cham (2019)"},{"key":"617_CR16","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-21690-4_4","volume-title":"Computer Aided Verification","author":"D Dietsch","year":"2015","unstructured":"Dietsch, D., Heizmann, M., Langenfeld, V., Podelski, A.: Fairness modulo theory: a new approach to ltl software model checking. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) Computer Aided Verification, pp. 49\u201366. Springer, Cham (2015)"},{"key":"617_CR17","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-68690-5_8","volume-title":"Formal Methods and Software Engineering","author":"Z Duan","year":"2017","unstructured":"Duan, Z., Tian, C., Duan, Z.: Verifying temporal properties of c programs via lazy abstraction. In: Duan, Z., Ong, L. (eds.) Formal Methods and Software Engineering, pp. 122\u2013139. Springer, Cham (2017)"},{"key":"617_CR18","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0\u2014a framework for LTL and $$\\omega $$-automata manipulation. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201916), Lecture Notes in Computer Science, vol. 9938, pp. 122\u2013129. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"617_CR19","doi-asserted-by":"publisher","unstructured":"Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 21st International Conference on Software Engineering (IEEE Cat. No.99CB37002), pp. 411\u2013420 (1999). https:\/\/doi.org\/10.1145\/302405.302672","DOI":"10.1145\/302405.302672"},{"key":"617_CR20","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/j.jlamp.2018.11.005","volume":"104","author":"H Garavel","year":"2019","unstructured":"Garavel, H.: Nested-unit petri nets. J. Log. Algebraic Methods Program. 104, 60\u201385 (2019). https:\/\/doi.org\/10.1016\/j.jlamp.2018.11.005","journal-title":"J. Log. Algebraic Methods Program."},{"key":"617_CR21","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-319-23820-3_28","volume-title":"Runtime Verification","author":"M Geske","year":"2015","unstructured":"Geske, M., Isberner, M., Steffen, B.: Rigorous examination of reactive systems. In: Bartocci, E., Majumdar, R. (eds.) Runtime Verification, pp. 423\u2013429. Springer, Cham (2015)"},{"key":"617_CR22","doi-asserted-by":"crossref","unstructured":"Geske, M., Jasper, M., Steffen, B., Howar, F., Schordan, M., van\u00a0de Pol, J.: RERS 2016: parallel and sequential benchmarks with focus on LTL verification. In: ISoLA. LNCS, vol 9953, pp. 787\u2013803. Springer (2016)","DOI":"10.1007\/978-3-319-47169-3_59"},{"key":"617_CR23","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Sytems\u2014FORTE 2002","author":"D Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: improving translation of ltl formulae to b\u00fcchi automata. In: Peled, D.A., Vardi, M.Y. (eds.) Formal Techniques for Networked and Distributed Sytems\u2014FORTE 2002, pp. 308\u2013326. Springer, Berlin (2002)"},{"key":"617_CR24","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"G Holzmann","year":"2011","unstructured":"Holzmann, G.: The SPIN Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional, Boston (2011)","edition":"1"},{"key":"617_CR25","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.228","author":"GJ Holzmann","year":"2001","unstructured":"Holzmann, G.J., Smith, M.H.: Software model checking: extracting verification models from source code. Softw. Test. Verif. Reliab. (2001). https:\/\/doi.org\/10.1002\/stvr.228","journal-title":"Softw. Test. Verif. Reliab."},{"key":"617_CR26","doi-asserted-by":"publisher","first-page":"608","DOI":"10.1007\/978-3-642-34026-0_45","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change","author":"F Howar","year":"2012","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D.: The rers grey-box challenge 2012: analysis of event-condition-action systems. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change, pp. 608\u2013614. Springer, Berlin (2012)"},{"key":"617_CR27","doi-asserted-by":"crossref","unstructured":"Howar, F., Isberner, M., Merten, M., Steffen, B., Beyer, D., P\u0103s\u0103reanu, C.: Rigorous examination of reactive systems. The RERS challenges 2012 and 2013. STTT 16(5), 457\u2013464 (2014)","DOI":"10.1007\/s10009-014-0337-y"},{"key":"617_CR28","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1007\/978-3-642-16558-0_55","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"F Howar","year":"2010","unstructured":"Howar, F., Steffen, B., Merten, M.: From ZULU to RERS. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification, and Validation, pp. 687\u2013704. Springer, Berlin (2010)"},{"issue":"6","key":"617_CR29","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/s10009-015-0396-8","volume":"17","author":"M Huisman","year":"2015","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis 2012. STTT 17(6), 647\u2013657 (2015)","journal-title":"STTT"},{"key":"617_CR30","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-319-51641-7_9","volume-title":"Leveraging Applications of Formal Methods, Verification, and Validation","author":"M Jasper","year":"2016","unstructured":"Jasper, M.: Counterexample-guided prefix refinement analysis for program verification. In: Lamprecht, A.L. (ed.) Leveraging Applications of Formal Methods, Verification, and Validation, pp. 143\u2013155. Springer, Cham (2016)"},{"key":"617_CR31","doi-asserted-by":"publisher","unstructured":"Jasper, M., Fecke, M., Steffen, B., Schordan, M., Meijer, J., Pol, J.v.d., Howar, F., Siegel, S.F.: The RERS 2017 challenge and workshop (invited paper). In: Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software, SPIN 2017, pp. 11\u201320. ACM (2017). https:\/\/doi.org\/10.1145\/3092282.3098206","DOI":"10.1145\/3092282.3098206"},{"key":"617_CR32","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1007\/978-3-030-17502-3_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Jasper","year":"2019","unstructured":"Jasper, M., Mues, M., Murtovi, A., Schl\u00fcter, M., Howar, F., Steffen, B., Schordan, M., Hendriks, D., Schiffelers, R., Kuppens, H., Vaandrager, F.W.: Rers 2019: combining synthesis with real-world models. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 101\u2013115. Springer, Cham (2019)"},{"key":"617_CR33","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/978-3-030-03421-4_27","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"M Jasper","year":"2018","unstructured":"Jasper, M., Mues, M., Schl\u00fcter, M., Steffen, B., Howar, F.: Rers 2018: Ctl, ltl, and reachability. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Verification, pp. 433\u2013447. Springer, Cham (2018)"},{"key":"617_CR34","doi-asserted-by":"crossref","unstructured":"Jasper, M., Schordan, M.: Multi-core model checking of large-scale reactive systems using different state representations. In: ISoLA. LNCS, vol 9952, pp. 212\u2013226. Springer (2016)","DOI":"10.1007\/978-3-319-47166-2_15"},{"key":"617_CR35","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-030-03421-4_16","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation. Verification","author":"M Jasper","year":"2018","unstructured":"Jasper, M., Steffen, B.: Synthesizing subtle bugs with known witnesses. In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation. Verification, pp. 235\u2013257. Springer, Cham (2018)"},{"issue":"1","key":"617_CR36","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1609\/aimag.v33i1.2395","volume":"33","author":"M J\u00e4rvisalo","year":"2012","unstructured":"J\u00e4rvisalo, M., Le Berre, D., Roussel, O., Simon, L.: The international SAT solver competitions. AI Mag. 33(1), 89\u201392 (2012). https:\/\/doi.org\/10.1609\/aimag.v33i1.2395","journal-title":"AI Mag."},{"key":"617_CR37","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-662-46681-0_61","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Kant","year":"2015","unstructured":"Kant, G., Laarman, A., Meijer, J., van de Pol, J., Blom, S., van Dijk, T.: Ltsmin: high-performance language-independent model checking. In: Baier, C., Tinelli, C. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 692\u2013707. Springer, Berlin (2015)"},{"issue":"7","key":"617_CR38","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976). https:\/\/doi.org\/10.1145\/360248.360252","journal-title":"Commun. ACM"},{"key":"617_CR39","doi-asserted-by":"publisher","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Lazy code motion. In: Proceedings of the ACM SIGPLAN\u201992 Conference on Programming Language Design and Implementation (PLDI), pp. 224\u2013234. ACM (1992). https:\/\/doi.org\/10.1145\/143095.143136","DOI":"10.1145\/143095.143136"},{"key":"617_CR40","first-page":"71","volume":"1","author":"J Knoop","year":"1993","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Lazy strength reduction. J. Program. Lang. 1, 71\u201391 (1993)","journal-title":"J. Program. Lang."},{"key":"617_CR41","doi-asserted-by":"publisher","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Partial dead code elimination. In: Proceedings of the ACM SIGPLAN\u201994 Conference on Programming Language Design and Implementation (PLDI), pp. 147\u2013158. ACM (1994). https:\/\/doi.org\/10.1145\/178243.178256","DOI":"10.1145\/178243.178256"},{"key":"617_CR42","doi-asserted-by":"publisher","unstructured":"Knoop, J., R\u00fcthing, O., Steffen, B.: Expansion-based removal of semantic partial redundancies. In: Compiler Construction, 8th International Conference, CC\u201999, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201999, Amsterdam, The Netherlands, 22\u201328 March, 1999, Proceedings, LNCS, vol. 1575, pp. 91\u2013106. Springer (1999). https:\/\/doi.org\/10.1007\/b72146","DOI":"10.1007\/b72146"},{"key":"617_CR43","doi-asserted-by":"crossref","unstructured":"Kordon, F., Linard, A., Buchs, D., Colange, M., Evangelista, S., Lampka, K., Lohmann, N., Paviot-Adet, E., Thierry-Mieg, Y., Wimmel, H.: Report on the model checking contest at petri nets 2011. In: Transactions on Petri Nets and Other Models of Concurrency VI. LNCS, vol 7400, pp. 169\u2013196. Springer (2012)","DOI":"10.1007\/978-3-642-35179-2_8"},{"key":"617_CR44","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-030-30942-8_13","volume-title":"Formal Methods\u2014The Next 30 Years","author":"F Lang","year":"2019","unstructured":"Lang, F., Mateescu, R., Mazzanti, F.: Compositional verification of concurrent systems by combining bisimulations. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) Formal Methods\u2014The Next 30 Years, pp. 196\u2013213. Springer, Cham (2019)"},{"key":"617_CR45","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-030-45237-7_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Lang","year":"2020","unstructured":"Lang, F., Mateescu, R., Mazzanti, F.: Sharp congruences adequate with temporal logics combining weak and strong modalities. In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, pp. 57\u201376. Springer, Cham (2020)"},{"key":"617_CR46","doi-asserted-by":"crossref","unstructured":"Larsen, K.G.: Modal specifications. In: CAV. LNCS, vol 407, pp. 232\u2013246. Springer (1989)","DOI":"10.1007\/3-540-52148-8_19"},{"key":"617_CR47","doi-asserted-by":"publisher","unstructured":"Meijer, J.: Efficient Learning and Analysis of System Behavior. Ph.D. thesis, University of Twente, Netherlands (2019). https:\/\/doi.org\/10.3990\/1.9789036548441","DOI":"10.3990\/1.9789036548441"},{"key":"617_CR48","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1007\/978-3-319-77935-5_24","volume-title":"NASA Formal Methods","author":"J Meijer","year":"2018","unstructured":"Meijer, J., van de Pol, J.: Sound black-box checking in the learnlib. In: Dutle, A., Mu\u00f1oz, C., Narkawicz, A. (eds.) NASA Formal Methods, pp. 349\u2013366. Springer, Cham (2018)"},{"issue":"2","key":"617_CR49","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1145\/359060.359069","volume":"22","author":"E Morel","year":"1979","unstructured":"Morel, E., Renvoise, C.: Global optimization by suppression of partial redundancies. Commun. ACM 22(2), 96\u2013103 (1979). https:\/\/doi.org\/10.1145\/359060.359069","journal-title":"Commun. ACM"},{"key":"617_CR50","unstructured":"Morse, J.: Expressive and Efficient Bounded Model Checking of Concurrent Software. Ph.D. thesis, University of Southampton (2015). http:\/\/eprints.soton.ac.uk\/id\/eprint\/379284"},{"issue":"5","key":"617_CR51","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-014-0335-0","volume":"16","author":"J Morse","year":"2014","unstructured":"Morse, J., Cordeiro, L., Nicole, D., Fischer, B.: Applying symbolic bounded model checking to the 2012 RERS Greybox challenge. Int. J. Softw. Tools Technol. Transf. 16(5), 519\u2013529 (2014)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"617_CR52","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Berlin (1999)"},{"key":"617_CR53","volume-title":"Petri Net Theory and the Modeling of Systems","author":"JL Peterson","year":"1981","unstructured":"Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice Hall PTR, Hoboken (1981)"},{"key":"617_CR54","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (SFCS 1977), pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"617_CR55","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201989, pp. 179\u2013190. ACM (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"617_CR56","doi-asserted-by":"publisher","unstructured":"van\u00a0de Pol, J., Meijer, J.: Synchronous or Alternating?, pp. 417\u2013430. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-22348-9_24","DOI":"10.1007\/978-3-030-22348-9_24"},{"issue":"5","key":"617_CR57","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/s10009-014-0324-3","volume":"16","author":"J van de Pol","year":"2014","unstructured":"van de Pol, J., Ruys, T.C., te Brinke, S.: Thoughtful Brute-force attack of the RERS 2012 and 2013 challenges. Int. J. Softw. Tools Technol. Transf. 16(5), 481\u2013491 (2014). https:\/\/doi.org\/10.1007\/s10009-014-0324-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"617_CR58","doi-asserted-by":"publisher","unstructured":"Rosen, B.K., Wegman, M.N., Zadeck, F.K.: Global value numbers and redundant computations. In: Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM (1988). https:\/\/doi.org\/10.1145\/73560.73562","DOI":"10.1145\/73560.73562"},{"issue":"5","key":"617_CR59","doi-asserted-by":"publisher","first-page":"493","DOI":"10.1007\/s10009-014-0338-x","volume":"16","author":"M Schordan","year":"2014","unstructured":"Schordan, M., Prantl, A.: Combining static analysis and state transition graphs for verification of event-condition-action systems in the RERS 2012 and 2013 challenges. Int. J. Softw. Tools Technol. Transf. 16(5), 493\u2013505 (2014). https:\/\/doi.org\/10.1007\/s10009-014-0338-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"617_CR60","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-61739-6_31","volume-title":"Static Analysis","author":"B Steffen","year":"1996","unstructured":"Steffen, B.: Property-oriented expansion. In: Cousot, R., Schmidt, D.A. (eds.) Static Analysis, pp. 22\u201341. Springer, Berlin (1996)"},{"key":"617_CR61","doi-asserted-by":"crossref","unstructured":"Steffen, B., Howar, F., Isberner, M., Naujokat, S., Margaria, T.: Tailored generation of concurrent benchmarks. STTT 16(5), 543\u2013558 (2014)","DOI":"10.1007\/s10009-014-0339-9"},{"key":"617_CR62","doi-asserted-by":"publisher","unstructured":"Steffen, B., Howar, F., Merten, M.: Introduction to Active Automata Learning from a Practical Perspective, pp. 256\u2013296. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-21455-4_8","DOI":"10.1007\/978-3-642-21455-4_8"},{"key":"617_CR63","doi-asserted-by":"crossref","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation. In: Bartocci, E., Ramakrishnan, C.R. (eds.) Model Checking Software, pp. 341\u2013357. Springer, Berlin (2013)","DOI":"10.1007\/978-3-642-39176-7_21"},{"issue":"5","key":"617_CR64","doi-asserted-by":"publisher","first-page":"465","DOI":"10.1007\/s10009-014-0336-z","volume":"16","author":"B Steffen","year":"2014","unstructured":"Steffen, B., Isberner, M., Naujokat, S., Margaria, T., Geske, M.: Property-driven benchmark generation: synthesizing programs of realistic structure. STTT 16(5), 465\u2013479 (2014)","journal-title":"STTT"},{"key":"617_CR65","doi-asserted-by":"crossref","unstructured":"Steffen, B., Jasper, M.: Property-preserving parallel decomposition. In: Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 125\u2013145. Springer (2017)","DOI":"10.1007\/978-3-319-63121-9_7"},{"key":"617_CR66","doi-asserted-by":"publisher","unstructured":"Steffen, B., Jasper, M.: Generating Hard Benchmark Problems for Weak Bisimulation, pp. 126\u2013145. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31514-6_8","DOI":"10.1007\/978-3-030-31514-6_8"},{"key":"617_CR67","doi-asserted-by":"publisher","unstructured":"Steffen, B., Jasper, M., Meijer, J., van\u00a0de Pol, J.: Property-preserving generation of tailored benchmark petri nets. In: 17th International Conference on Application of Concurrency to System Design (ACSD), pp. 1\u20138 (2017). https:\/\/doi.org\/10.1109\/ACSD.2017.24","DOI":"10.1109\/ACSD.2017.24"},{"key":"617_CR68","doi-asserted-by":"publisher","unstructured":"Steffen, B., Knoop, J.: Finite Constants: Characterizations of a New Decidable Set of Constants. In: Kreczmar, A., Mirkowska, G. (eds.) Mathematical Foundations of Computer Science (MFCS\u201989), LNCS, vol. 379, pp. 481\u2013491. Springer (1989). https:\/\/doi.org\/10.1007\/3-540-51486-4_94","DOI":"10.1007\/3-540-51486-4_94"},{"key":"617_CR69","doi-asserted-by":"publisher","unstructured":"Wang, M., Tian, C., Duan, Z.: Full regular temporal property verification as dynamic program execution. In: IEEE\/ACM 39th International Conference on Software Engineering Companion (ICSE-C), pp. 226\u2013228 (2017). https:\/\/doi.org\/10.1109\/ICSE-C.2017.98","DOI":"10.1109\/ICSE-C.2017.98"},{"issue":"3","key":"617_CR70","doi-asserted-by":"publisher","first-page":"1101","DOI":"10.1109\/TR.2018.2876333","volume":"68","author":"M Wang","year":"2019","unstructured":"Wang, M., Tian, C., Zhang, N., Duan, Z.: Verifying full regular temporal properties of programs via dynamic program execution. IEEE Trans. Reliab. 68(3), 1101\u20131116 (2019). https:\/\/doi.org\/10.1109\/TR.2018.2876333","journal-title":"IEEE Trans. Reliab."},{"key":"617_CR71","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1016\/j.tcs.2019.12.038","volume":"809","author":"M Wang","year":"2020","unstructured":"Wang, M., Tian, C., Zhang, N., Duan, Z., Yao, C.: Translating Xd-C programs to MSVL programs. Theor. Comput. Sci. 809, 430\u2013465 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2019.12.038","journal-title":"Theor. Comput. Sci."},{"issue":"1","key":"617_CR72","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1016\/S0019-9958(83)80051-5","volume":"56","author":"P Wolper","year":"1983","unstructured":"Wolper, P.: Temporal logic can be more expressive. Inf. Control 56(1), 72\u201399 (1983). https:\/\/doi.org\/10.1016\/S0019-9958(83)80051-5","journal-title":"Inf. Control"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00617-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-021-00617-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-021-00617-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,12,26]],"date-time":"2021-12-26T12:03:11Z","timestamp":1640520191000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-021-00617-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,6,24]]},"references-count":72,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2021,12]]}},"alternative-id":["617"],"URL":"https:\/\/doi.org\/10.1007\/s10009-021-00617-z","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021,6,24]]},"assertion":[{"value":"6 May 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 June 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}