{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:05:15Z","timestamp":1762459515671,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":40,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,7,13]],"date-time":"2017-07-13T00:00:00Z","timestamp":1499904000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2017,7,13]]},"DOI":"10.1145\/3092282.3098206","type":"proceedings-article","created":{"date-parts":[[2017,7,13]],"date-time":"2017-07-13T13:45:49Z","timestamp":1499953549000},"page":"11-20","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["The RERS 2017 challenge and workshop (invited paper)"],"prefix":"10.1145","author":[{"given":"Marc","family":"Jasper","sequence":"first","affiliation":[{"name":"Lawrence Livermore National Laboratory, USA \/ TU Dortmund, Germany"}]},{"given":"Maximilian","family":"Fecke","sequence":"additional","affiliation":[{"name":"Lawrence Livermore National Laboratory, USA \/ TU Dortmund, Germany"}]},{"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[{"name":"TU Dortmund, Germany"}]},{"given":"Markus","family":"Schordan","sequence":"additional","affiliation":[{"name":"Lawrence Livermore National Laboratory, USA"}]},{"given":"Jeroen","family":"Meijer","sequence":"additional","affiliation":[{"name":"University of Twente, Netherlands"}]},{"given":"Jaco van de","family":"Pol","sequence":"additional","affiliation":[{"name":"University of Twente, Netherlands"}]},{"given":"Falk","family":"Howar","sequence":"additional","affiliation":[{"name":"TU Clausthal, Germany"}]},{"given":"Stephen F.","family":"Siegel","sequence":"additional","affiliation":[{"name":"University of Delaware, USA"}]}],"member":"320","published-online":{"date-parts":[[2017,7,13]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_25"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-9_55"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2814270.2814303"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2001252.2001255"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","unstructured":"M. Broy B. Jonsson J.-P. Katoen M. Leucker and A. Pretschner (Eds.). 2005. Model-Based Testing of Reactive Systems. Springer.   M. Broy B. Jonsson J.-P. Katoen M. Leucker and A. Pretschner (Eds.). 2005. Model-Based Testing of Reactive Systems. Springer.","DOI":"10.1007\/b137241"},{"key":"e_1_3_2_1_7_1","unstructured":"E. M. Clarke O. Grumberg and D. Peled. 2001. Model Checking. MIT Press. I\u2013XIV 1\u2013314 pages.  E. M. Clarke O. Grumberg and D. Peled. 2001. Model Checking. MIT Press. I\u2013XIV 1\u2013314 pages."},{"key":"e_1_3_2_1_8_1","unstructured":"Mike Czech Eyke H\u00fcllermeier Marie-Christine Jakobs and Heike Wehrheim. 2017.  Mike Czech Eyke H\u00fcllermeier Marie-Christine Jakobs and Heike Wehrheim. 2017."},{"key":"e_1_3_2_1_9_1","volume-title":"CoRR abs\/1703.00757","author":"Software Verification Competitions Predicting Rankings","year":"2017","unstructured":"Predicting Rankings of Software Verification Competitions . CoRR abs\/1703.00757 ( 2017 ). http:\/\/arxiv.org\/abs\/1703.00757 Predicting Rankings of Software Verification Competitions. CoRR abs\/1703.00757 (2017). http:\/\/arxiv.org\/abs\/1703.00757"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_3_2_1_11_1","volume-title":"Accessed","author":"de Sande F.","year":"2004","unstructured":"F. de Sande . 2004 . https:\/\/sourceforge.net\/projects\/ompscr\/. (2004). OpenMP Source Code Repository, file c_fft6.c . Accessed May 22, 2017. F. de Sande. 2004. https:\/\/sourceforge.net\/projects\/ompscr\/. (2004). OpenMP Source Code Repository, file c_fft6.c. Accessed May 22, 2017."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0264-5"},{"key":"e_1_3_2_1_13_1","volume-title":"Runtime Verification: 6th International Conference. Springer, 423\u2013429","author":"Geske Maren","year":"2015","unstructured":"Maren Geske , Malte Isberner , and Bernhard Steffen . 2015 . Rigorous Examination of Reactive Systems: The RERS Challenge 2015 . In Runtime Verification: 6th International Conference. Springer, 423\u2013429 . Maren Geske, Malte Isberner, and Bernhard Steffen. 2015. Rigorous Examination of Reactive Systems: The RERS Challenge 2015. In Runtime Verification: 6th International Conference. Springer, 423\u2013429."},{"volume-title":"RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification. In International Symposium on Leveraging Applications of Formal Methods. Springer, 787\u2013803","author":"Geske Maren","key":"e_1_3_2_1_14_1","unstructured":"Maren Geske , Marc Jasper , Bernhard Steffen , Falk Howar , Markus Schordan , and Jaco van de Pol. 2016 . RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification. In International Symposium on Leveraging Applications of Formal Methods. Springer, 787\u2013803 . Maren Geske, Marc Jasper, Bernhard Steffen, Falk Howar, Markus Schordan, and Jaco van de Pol. 2016. RERS 2016: Parallel and Sequential Benchmarks with Focus on LTL Verification. In International Symposium on Leveraging Applications of Formal Methods. Springer, 787\u2013803."},{"key":"e_1_3_2_1_15_1","volume-title":"CAV 2008 Workshop on \u201cExploiting Concurrency Efficiently and Correctly\u201d","author":"Godefroid Patrice","year":"2008","unstructured":"Patrice Godefroid and Nachiappan Nagappan . 2008 . Concurrency at Microsoft \u2014 An Exploratory Survey. In (EC) 2 , CAV 2008 Workshop on \u201cExploiting Concurrency Efficiently and Correctly\u201d . Princeton. https:\/\/patricegodefroid.github.io\/public_ psfiles\/ec2.pdf. Patrice Godefroid and Nachiappan Nagappan. 2008. Concurrency at Microsoft \u2014 An Exploratory Survey. In (EC) 2, CAV 2008 Workshop on \u201cExploiting Concurrency Efficiently and Correctly\u201d. Princeton. https:\/\/patricegodefroid.github.io\/public_ psfiles\/ec2.pdf."},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622420.1622423"},{"volume-title":"Using Features Of Models To Improve State Space Exploration. Master\u2019s thesis","author":"Heijblom Richard","key":"e_1_3_2_1_17_1","unstructured":"Richard Heijblom . 2016. Using Features Of Models To Improve State Space Exploration. Master\u2019s thesis . University of Twente . Richard Heijblom. 2016. Using Features Of Models To Improve State Space Exploration. Master\u2019s thesis. University of Twente."},{"volume-title":"The origin of concurrent programming","author":"Richard Hoare Charles Antony","key":"e_1_3_2_1_18_1","unstructured":"Charles Antony Richard Hoare . 1978. Communicating Sequential Processes . In The origin of concurrent programming . Springer , 413\u2013443. Charles Antony Richard Hoare. 1978. Communicating Sequential Processes. In The origin of concurrent programming. Springer, 413\u2013443."},{"key":"e_1_3_2_1_19_1","volume-title":"The SPIN Model Checker: Primer and Reference Manual","author":"Holzmann Gerard","unstructured":"Gerard Holzmann . 2011. The SPIN Model Checker: Primer and Reference Manual ( 1 st ed.). Addison-Wesley Professional . Gerard Holzmann. 2011. The SPIN Model Checker: Primer and Reference Manual (1st ed.). Addison-Wesley Professional.","edition":"1"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"crossref","unstructured":"G. J. Holzmann and M. H. Smith. 2001. Software Model Checking: Extracting Verification Models from Source Code. Softw. Testing Verification and Reliability 11 2 (2001).  G. J. Holzmann and M. H. Smith. 2001. Software Model Checking: Extracting Verification Models from Source Code. Softw. Testing Verification and Reliability 11 2 (2001).","DOI":"10.1002\/stvr.228"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-34026-0_45"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0337-y"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0396-8"},{"key":"e_1_3_2_1_24_1","volume-title":"Multi-core Model Checking of Largescale Reactive Systems Using Different State Representations. In International Symposium on Leveraging Applications of Formal Methods. Springer, 212\u2013226","author":"Jasper Marc","year":"2016","unstructured":"Marc Jasper and Markus Schordan . 2016 . Multi-core Model Checking of Largescale Reactive Systems Using Different State Representations. In International Symposium on Leveraging Applications of Formal Methods. Springer, 212\u2013226 . Marc Jasper and Markus Schordan. 2016. Multi-core Model Checking of Largescale Reactive Systems Using Different State Representations. In International Symposium on Leveraging Applications of Formal Methods. Springer, 212\u2013226."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2150976.2150997"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_27_1","unstructured":"F. Kordon H. Garavel L. M. Hillah F. Hulin-Hubard G. Chiardo A. Hamez L. Jezequel A. Miner J. Meijer E. Paviot-Adet D. Racordon C. Rodriguez C. Rohr J. Srba Y. Thierry-Mieg G. Tri.nh and K. Wolf. 2016. Complete Results for the 2016 Edition of the Model Checking Contest. http:\/\/mcc.lip6.fr\/2016\/results.php. (June 2016).  F. Kordon H. Garavel L. M. Hillah F. Hulin-Hubard G. Chiardo A. Hamez L. Jezequel A. Miner J. Meijer E. Paviot-Adet D. Racordon C. Rodriguez C. Rohr J. Srba Y. Thierry-Mieg G. Tri.nh and K. Wolf. 2016. Complete Results for the 2016 Edition of the Model Checking Contest. http:\/\/mcc.lip6.fr\/2016\/results.php. (June 2016)."},{"key":"e_1_3_2_1_28_1","volume-title":"Modal Specifications. In International Conference on Computer Aided Verification. Springer, 232\u2013246","author":"Larsen Kim Guldstrand","year":"1989","unstructured":"Kim Guldstrand Larsen . 1989 . Modal Specifications. In International Conference on Computer Aided Verification. Springer, 232\u2013246 . Kim Guldstrand Larsen. 1989. Modal Specifications. In International Conference on Computer Aided Verification. Springer, 232\u2013246."},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2010.177"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250738"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"crossref","unstructured":"F. Nielson H. R. Nielson and C. Hankin. 1999. Principles of Program Analysis. Springer.   F. Nielson H. R. Nielson and C. Hankin. 1999. Principles of Program Analysis. Springer.","DOI":"10.1007\/978-3-662-03811-6"},{"volume-title":"Petri Net Theory and the Modeling of Systems","author":"Peterson James Lyle","key":"e_1_3_2_1_32_1","unstructured":"James Lyle Peterson . 1981. Petri Net Theory and the Modeling of Systems . Prentice Hall PTR , Upper Saddle River, NJ, USA. James Lyle Peterson. 1981. Petri Net Theory and the Modeling of Systems. Prentice Hall PTR, Upper Saddle River, NJ, USA."},{"key":"e_1_3_2_1_33_1","unstructured":"Louis-Noel Pouchet. 2012. PolyOpt\/C 0.2.1: a Polyhedral Compiler for ROSE. http:\/\/web.cs.ucla.edu\/~pouchet\/software\/polyopt\/. (2012).  Louis-Noel Pouchet. 2012. PolyOpt\/C 0.2.1: a Polyhedral Compiler for ROSE. http:\/\/web.cs.ucla.edu\/~pouchet\/software\/polyopt\/. (2012)."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/349214.349241"},{"volume-title":"International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (LNCS 8803)","author":"Schordan Markus","key":"e_1_3_2_1_35_1","unstructured":"Markus Schordan , Pei-Hung Lin , Dan Quinlan , and Louis-No\u00ebl Pouchet . 2014. Verification of Polyhedral Optimizations with Constant Loop Bounds in Finite State Space Computations . In International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (LNCS 8803) . Springer , 493\u2013508. Markus Schordan, Pei-Hung Lin, Dan Quinlan, and Louis-No\u00ebl Pouchet. 2014. Verification of Polyhedral Optimizations with Constant Loop Bounds in Finite State Space Computations. In International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (LNCS 8803). Springer, 493\u2013508."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/2807591.2807635"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0339-9"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-014-0336-z"},{"volume-title":"LNCS (to appear)","author":"Steffen Bernhard","key":"e_1_3_2_1_39_1","unstructured":"Bernhard Steffen and Marc Jasper . 2017. Property-Preserving Parallel Decomposition . In LNCS (to appear) . Springer . Bernhard Steffen and Marc Jasper. 2017. Property-Preserving Parallel Decomposition. In LNCS (to appear). Springer."},{"volume-title":"Proceedings of ACSD 2017 (to appear). IEEE Computer Society.","author":"Steffen Bernhard","key":"e_1_3_2_1_40_1","unstructured":"Bernhard Steffen , Marc Jasper , Jaco van de Pol, and Jeroen Meijer. 2017. Property-Preserving Generation of Tailored Benchmark Petri Nets . In Proceedings of ACSD 2017 (to appear). IEEE Computer Society. Bernhard Steffen, Marc Jasper, Jaco van de Pol, and Jeroen Meijer. 2017. Property-Preserving Generation of Tailored Benchmark Petri Nets. In Proceedings of ACSD 2017 (to appear). IEEE Computer Society."}],"event":{"name":"ISSTA '17: International Symposium on Software Testing and Analysis","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"],"location":"Santa Barbara CA USA","acronym":"ISSTA '17"},"container-title":["Proceedings of the 24th ACM SIGSOFT International SPIN Symposium on Model Checking of Software"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3092282.3098206","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3092282.3098206","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:03:08Z","timestamp":1750215788000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3092282.3098206"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,13]]},"references-count":40,"alternative-id":["10.1145\/3092282.3098206","10.1145\/3092282"],"URL":"https:\/\/doi.org\/10.1145\/3092282.3098206","relation":{},"subject":[],"published":{"date-parts":[[2017,7,13]]},"assertion":[{"value":"2017-07-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}