{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,4]],"date-time":"2025-10-04T18:09:21Z","timestamp":1759601361848,"version":"3.40.3"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030837228"},{"type":"electronic","value":"9783030837235"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-83723-5_16","type":"book-chapter","created":{"date-parts":[[2021,8,4]],"date-time":"2021-08-04T06:02:58Z","timestamp":1628056978000},"page":"242-263","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Every Component Matters: Generating Parallel Verification Benchmarks with Hardness Guarantees"],"prefix":"10.1007","author":[{"given":"Marc","family":"Jasper","sequence":"first","affiliation":[]},{"given":"Maximilian","family":"Schl\u00fcter","sequence":"additional","affiliation":[]},{"given":"David","family":"Schmidt","sequence":"additional","affiliation":[]},{"given":"Bernhard","family":"Steffen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,8,5]]},"reference":[{"key":"16_CR1","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":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-642-28872-2_3","volume-title":"Fundamental Approaches to Software Engineering","author":"SS Bauer","year":"2012","unstructured":"Bauer, S.S., et al.: Moving from specifications to contracts in component-based design. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 43\u201358. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-28872-2_3"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-319-63121-9_12","volume-title":"Models, Algorithms, Logics and Tools","author":"A Benveniste","year":"2017","unstructured":"Benveniste, A., Caillaud, B.: Synchronous interfaces and assume\/guarantee contracts. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 233\u2013248. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_12"},{"issue":"2\u20133","key":"16_CR4","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1561\/1000000053","volume":"12","author":"A Benveniste","year":"2018","unstructured":"Benveniste, A., et al.: Contracts for system design. Found. Trends Electron. Des. Autom. 12(2\u20133), 124\u2013400 (2018). https:\/\/doi.org\/10.1561\/1000000053","journal-title":"Found. Trends Electron. Des. Autom."},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-030-55754-6_20","volume-title":"NASA Formal Methods","author":"RC Cardoso","year":"2020","unstructured":"Cardoso, R.C., Farrell, M., Luckcuck, M., Ferrando, A., Fisher, M.: Heterogeneous verification of an autonomous curiosity rover. In: Lee, R., Jha, S., Mavridou, A., Giannakopoulou, D. (eds.) NFM 2020. LNCS, vol. 12229, pp. 353\u2013360. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-55754-6_20"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Chandra, S., Godefroid, P., Palm, C.: Software model checking in practice: an industrial case study. In: Proceedings of the 24th International Conference on Software Engineering, ICSE 2002, pp. 431\u2013441 (2002). https:\/\/doi.org\/10.1145\/581339.581393","DOI":"10.1145\/581339.581393"},{"key":"16_CR7","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":"16_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"787","DOI":"10.1007\/978-3-319-47169-3_59","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications","author":"M Geske","year":"2016","unstructured":"Geske, M., Jasper, M., Steffen, B., Howar, F., Schordan, M., van de Pol, J.: RERS 2016: parallel and sequential benchmarks with focus on LTL verification. In: Margaria, T., Steffen, B. (eds.) ISoLA 2016. LNCS, vol. 9953, pp. 787\u2013803. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-47169-3_59"},{"issue":"5","key":"16_CR9","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1145\/940071.940106","volume":"28","author":"D Giannakopoulou","year":"2003","unstructured":"Giannakopoulou, D., Magee, J.: Fluent model checking for event-based systems. ACM SIGSOFT Softw. Eng. Notes 28(5), 257\u2013266 (2003). https:\/\/doi.org\/10.1145\/940071.940106","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"16_CR10","doi-asserted-by":"publisher","unstructured":"Goga, N., Costache, S., Moldoveanu, F.: A formal analysis of ISO\/IEEE P11073-20601 standard of medical device communication. In: 3rd Annual IEEE Systems Conference, pp. 163\u2013166 (2009). https:\/\/doi.org\/10.1109\/SYSTEMS.2009.4815792","DOI":"10.1109\/SYSTEMS.2009.4815792"},{"issue":"3","key":"16_CR11","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. (TOPLAS) 16(3), 843\u2013871 (1994). https:\/\/doi.org\/10.1145\/177492.177725","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"key":"16_CR12","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: Communicating sequential processes. In: The Origin of Concurrent Programming, pp. 413\u2013443. Springer (1978). https:\/\/doi.org\/10.1145\/359576.359585","DOI":"10.1145\/359576.359585"},{"key":"16_CR13","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"},{"issue":"5","key":"16_CR14","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/s10009-014-0337-y","volume":"16","author":"F Howar","year":"2014","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). https:\/\/doi.org\/10.1007\/s10009-014-0337-y","journal-title":"STTT"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Howar, F., Jasper, M., Mues, M., Schmidt, D., Steffen, B.: The RERS challenge: towards controllable and scalable benchmark synthesis. Int. J. Softw. Tools Technol. Transfer. (2021). https:\/\/doi.org\/10.1007\/s10009-021-00617-z","DOI":"10.1007\/s10009-021-00617-z"},{"key":"16_CR16","doi-asserted-by":"publisher","unstructured":"Jasper, M., et al.: 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":"16_CR17","series-title":"Lecture Notes in Computer Science","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., et al.: RERS 2019: combining synthesis with real-world models. In: Beyer, D., Huisman, M., Kordon, F., Steffen, B. (eds.) TACAS 2019. LNCS, vol. 11429, pp. 101\u2013115. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-17502-3_7"},{"key":"16_CR18","series-title":"Lecture Notes in Computer Science","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.) ISoLA 2018. LNCS, vol. 11245, pp. 433\u2013447. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_27"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","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.) ISoLA 2018. LNCS, vol. 11245, pp. 235\u2013257. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03421-4_16"},{"key":"16_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-642-35179-2_8","volume-title":"Transactions on Petri Nets and Other Models of Concurrency VI","author":"F Kordon","year":"2012","unstructured":"Kordon, F., et al.: Report on the model checking contest at Petri nets 2011. In: Jensen, K., van der Aalst, W.M., Ajmone Marsan, M., Franceschinis, G., Kleijn, J., Kristensen, L.M. (eds.) Transactions on Petri Nets and Other Models of Concurrency VI. LNCS, vol. 7400, pp. 169\u2013196. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-35179-2_8"},{"key":"16_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/978-3-030-30942-8_13","volume-title":"Formal Methods \u2013 The 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.) FM 2019. LNCS, vol. 11800, pp. 196\u2013213. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_13"},{"key":"16_CR22","doi-asserted-by":"publisher","unstructured":"Lang, F., Mateescu, R., Mazzanti, F.: Sharp congruences adequate with temporal logics combining weak and strong modalities. In: TACAS 2020. LNCS, vol. 12079, pp. 57\u201376. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_4","DOI":"10.1007\/978-3-030-45237-7_4"},{"key":"16_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/3-540-52148-8_19","volume-title":"Automatic Verification Methods for Finite State Systems","author":"KG Larsen","year":"1990","unstructured":"Larsen, K.G.: Modal specifications. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol. 407, pp. 232\u2013246. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52148-8_19"},{"key":"16_CR24","doi-asserted-by":"publisher","unstructured":"Guldstrand Larsen, K.: Ideal specification formalism = expressivity + compositionality + decidability + testability + ... In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 33\u201356. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0039050","DOI":"10.1007\/BFb0039050"},{"key":"16_CR25","unstructured":"Peterson, J.L.: Petri Net Theory and the Modeling of Systems. Prentice Hall PTR (1981)"},{"issue":"1\u20132","key":"16_CR26","doi-asserted-by":"publisher","first-page":"119","DOI":"10.3233\/FI-2011-416","volume":"108","author":"JB Raclet","year":"2011","unstructured":"Raclet, J.B., Badouel, E., Benveniste, A., Caillaud, B., Legay, A., Passerone, R.: A modal interface theory for component-based design. Fund. Inform. 108(1\u20132), 119\u2013149 (2011). https:\/\/doi.org\/10.3233\/FI-2011-416","journal-title":"Fund. Inform."},{"key":"16_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/978-3-030-53291-8_6","volume-title":"Computer Aided Verification","author":"SF Siegel","year":"2020","unstructured":"Siegel, S.F., Yan, Y.: Action-based model checking: logic, automata, and reduction. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 77\u2013100. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_6"},{"key":"16_CR28","doi-asserted-by":"publisher","unstructured":"Steffen, B., Jasper, M., Meijer, J., van de Pol, J.: Property-preserving generation of tailored benchmark Petri nets. In: 2017 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":"16_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-319-63121-9_7","volume-title":"Models, Algorithms, Logics and Tools","author":"B Steffen","year":"2017","unstructured":"Steffen, B., Jasper, M.: Property-preserving parallel decomposition. In: Aceto, L., Bacci, G., Bacci, G., Ing\u00f3lfsd\u00f3ttir, A., Legay, A., Mardare, R. (eds.) Models, Algorithms, Logics and Tools. LNCS, vol. 10460, pp. 125\u2013145. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63121-9_7"},{"key":"16_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-030-31514-6_8","volume-title":"From Reactive Systems to Cyber-Physical Systems","author":"B Steffen","year":"2019","unstructured":"Steffen, B., Jasper, M.: Generating hard benchmark problems for weak bisimulation. In: Bartocci, E., Cleaveland, R., Grosu, R., Sokolsky, O. (eds.) From Reactive Systems to Cyber-Physical Systems. LNCS, vol. 11500, pp. 126\u2013145. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31514-6_8"},{"key":"16_CR31","doi-asserted-by":"publisher","unstructured":"Warford, J.S., Vega, D., Staley, S.M.: A calculational deductive system for linear temporal logic. ACM Comput. Surv. 53(3) (2020). https:\/\/doi.org\/10.1145\/3387109","DOI":"10.1145\/3387109"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Tools and Trends"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-83723-5_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,8,4]],"date-time":"2021-08-04T06:09:31Z","timestamp":1628057371000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-83723-5_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030837228","9783030837235"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-83723-5_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"5 August 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}