{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,26]],"date-time":"2026-02-26T15:27:40Z","timestamp":1772119660851,"version":"3.50.1"},"reference-count":50,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,4,18]],"date-time":"2025-04-18T00:00:00Z","timestamp":1744934400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,4,18]],"date-time":"2025-04-18T00:00:00Z","timestamp":1744934400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["497132954"],"award-info":[{"award-number":["497132954"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["497132954"],"award-info":[{"award-number":["497132954"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001866","name":"Fonds National de la Recherche Luxembourg","doi-asserted-by":"publisher","award":["C22\/IS\/17432184"],"award-info":[{"award-number":["C22\/IS\/17432184"]}],"id":[{"id":"10.13039\/501100001866","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001866","name":"Fonds National de la Recherche Luxembourg","doi-asserted-by":"publisher","award":["C22\/IS\/17432184"],"award-info":[{"award-number":["C22\/IS\/17432184"]}],"id":[{"id":"10.13039\/501100001866","id-type":"DOI","asserted-by":"publisher"}]},{"name":"CISPA - Helmholtz-Zentrum f\u00fcr Informationssicherheit gGmbH"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>We present an algorithm for the repair of parameterized systems that can be represented as well-structured transition systems. The repair problem is, for a given process implementation, to find a refinement such that a given safety property is satisfied by the resulting parameterized system, and deadlocks are avoided. Our algorithm uses a parameterized model checker to determine the correctness of candidate solutions and employs a constraint system to rule out candidates. Parameterized systems that fall into our class include disjunctive systems, pairwise rendezvous systems, broadcast protocols, and certain global synchronization protocols. Moreover, we show that parameterized deadlock detection and similar global properties can be decided in EXPTIME for disjunctive systems, and that deadlock detection is in general undecidable for broadcast protocols.<\/jats:p>","DOI":"10.1007\/s10703-025-00469-2","type":"journal-article","created":{"date-parts":[[2025,4,18]],"date-time":"2025-04-18T02:03:57Z","timestamp":1744941837000},"page":"335-375","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Automatic WSTS-based repair and deadlock detection of parameterized systems"],"prefix":"10.1007","volume":"66","author":[{"given":"Tom","family":"Baumeister","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Swen","family":"Jacobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mouhammad","family":"Sakr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcus","family":"V\u00f6lp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,4,18]]},"reference":[{"issue":"4","key":"469_CR1","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/0020-0190(88)90211-6","volume":"28","author":"I Suzuki","year":"1988","unstructured":"Suzuki I (1988) Proving properties of a ring of finite state machines. Inf Process Lett 28(4):213\u2013214","journal-title":"Inf Process Lett"},{"issue":"3","key":"469_CR2","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1145\/146637.146681","volume":"39","author":"SM German","year":"1992","unstructured":"German SM, Sistla AP (1992) Reasoning about systems with many processes. J ACM 39(3):675\u2013735","journal-title":"J ACM"},{"key":"469_CR3","doi-asserted-by":"crossref","unstructured":"Esparza J, Finkel A, Mayr R (1999) On the verification of broadcast protocols. In: LICS, 352\u2013359. IEEE Computer Society","DOI":"10.1109\/LICS.1999.782630"},{"key":"469_CR4","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/10721959_19","volume-title":"Automated Deduction\u2014CADE-17","author":"EA Emerson","year":"2000","unstructured":"Emerson EA, Kahlon V (2000) Reducing Model Checking of the Many to the Few. Automated Deduction\u2014CADE-17. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 236\u2013254. https:\/\/doi.org\/10.1007\/10721959_19"},{"issue":"4","key":"469_CR5","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1142\/S0129054103001881","volume":"14","author":"EA Emerson","year":"2003","unstructured":"Emerson EA, Namjoshi KS (2003) On reasoning about rings. Found Comput Sci 14(4):527\u2013549","journal-title":"Found Comput Sci"},{"key":"469_CR6","doi-asserted-by":"crossref","unstructured":"Emerson EA, Kahlon V (2003) Model checking guarded protocols. In: LICS, 361\u2013370. IEEE Computer Society","DOI":"10.1109\/LICS.2003.1210076"},{"key":"469_CR7","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-540-28644-8_18","volume-title":"CONCUR 2004\u2014Concurrency Theory","author":"E Clarke","year":"2004","unstructured":"Clarke E, Talupur M, Touili T, Veith H (2004) Verification by Network Decomposition. In: Gardner P, Yoshida N (eds) CONCUR 2004\u2014Concurrency Theory. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 276\u2013291. https:\/\/doi.org\/10.1007\/978-3-540-28644-8_18"},{"key":"469_CR8","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-642-54013-4_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Aminof","year":"2014","unstructured":"Aminof B, Jacobs S, Khalimov A, Rubin S (2014) Parameterized Model Checking of Token-Passing Systems. In: McMillan KL, Rival X (eds) Verification, Model Checking, and Abstract Interpretation. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 262\u2013281. https:\/\/doi.org\/10.1007\/978-3-642-54013-4_15"},{"key":"469_CR9","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-3-662-44584-6_9","volume-title":"CONCUR 2014\u2014Concurrency Theory","author":"B Aminof","year":"2014","unstructured":"Aminof B, Kotek T, Rubin S, Spegni F, Veith H (2014) Parameterized Model Checking of Rendezvous Systems. In: Baldan P, Gorla D (eds) CONCUR 2014\u2014Concurrency Theory. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 109\u2013124. https:\/\/doi.org\/10.1007\/978-3-662-44584-6_9"},{"key":"469_CR10","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/978-3-319-40229-1_34","volume-title":"Automated Reasoning","author":"B Aminof","year":"2016","unstructured":"Aminof B, Rubin S (2016) Model Checking Parameterised Multi-token Systems via the Composition Method. In: Olivetti N, Tiwari A (eds) Automated Reasoning. Springer International Publishing, Cham, pp 499\u2013515. https:\/\/doi.org\/10.1007\/978-3-319-40229-1_34"},{"key":"469_CR11","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Computer Aided Verification","author":"B Jobstmann","year":"2005","unstructured":"Jobstmann B, Griesmayer A, Bloem R (2005) Program Repair as a Game. In: Etessami K, Rajamani SK (eds) Computer Aided Verification. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 226\u2013238. https:\/\/doi.org\/10.1007\/11513988_23"},{"issue":"2","key":"469_CR12","first-page":"1","volume":"17","author":"PC Attie","year":"2017","unstructured":"Attie PC, Bab KDA, Sakr M (2017) Model and program repair via sat solving. ACM Trans Embed Comput Syst (TECS) 17(2):1\u201325","journal-title":"ACM Trans Embed Comput Syst (TECS)"},{"key":"469_CR13","doi-asserted-by":"crossref","unstructured":"Bloem R, Hofferek G, K\u00f6nighofer B, K\u00f6nighofer R, Au\u00dferlechner S, Sp\u00f6rk R (2014) Synthesis of synchronization using uninterpreted functions. In: 2014 Formal Methods in Computer-Aided Design (FMCAD), 35\u201342. IEEE","DOI":"10.1109\/FMCAD.2014.6987593"},{"key":"469_CR14","doi-asserted-by":"publisher","first-page":"301","DOI":"10.1007\/978-3-319-63390-9_16","volume-title":"Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II","author":"J McClurg","year":"2017","unstructured":"McClurg J, Hojjat H, \u010cern\u00fd P (2017) Synchronization Synthesis for Network Programs. In: Majumdar R, Kun\u010dak V (eds) Computer Aided Verification: 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II. Springer International Publishing, Cham, pp 301\u2013321. https:\/\/doi.org\/10.1007\/978-3-319-63390-9_16"},{"key":"469_CR15","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-030-53288-8_15","volume-title":"Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21\u201324, 2020, Proceedings, Part I","author":"N Jaber","year":"2020","unstructured":"Jaber N, Jacobs S, Wagner C, Kulkarni M, Samanta R (2020) Parameterized Verification of Systems with Global Synchronization and Guards. In: Lahiri SK, Wang C (eds) Computer Aided Verification: 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21\u201324, 2020, Proceedings, Part I. Springer International Publishing, Cham, pp 299\u2013323. https:\/\/doi.org\/10.1007\/978-3-030-53288-8_15"},{"issue":"2","key":"469_CR16","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/0890-5401(90)90009-7","volume":"89","author":"A Finkel","year":"1990","unstructured":"Finkel A (1990) Reduction and covering of infinite reachability trees. Inf Comput 89(2):144\u2013179","journal-title":"Inf Comput"},{"key":"469_CR17","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Cerans K, Jonsson B. Tsay Y-K (1996) General decidability theorems for infinite-state systems. In: Proceedings 11th Annual IEEE Symposium on Logic in Computer Science, 313\u2013321. IEEE","DOI":"10.1109\/LICS.1996.561359"},{"issue":"1\u20132","key":"469_CR18","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A Finkel","year":"2001","unstructured":"Finkel A, Schnoebelen P (2001) Well-structured transition systems everywhere! Theoret Comput Sci 256(1\u20132):63\u201392","journal-title":"Theoret Comput Sci"},{"key":"469_CR19","unstructured":"Jacobs S, Sakr M, V\u00f6lp M (2022) Automatic repair and deadlock detection for parameterized systems. In: FMCAD"},{"key":"469_CR20","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-030-21571-2_20","volume-title":"Application and Theory of Petri Nets and Concurrency: 40th International Conference, PETRI NETS 2019, Aachen, Germany, June 23\u201328, 2019, Proceedings","author":"J Esparza","year":"2019","unstructured":"Esparza J, Raskin M, Weil-Kennedy C (2019) Parameterized Analysis of Immediate Observation Petri Nets. In: Donatelli S, Haar S (eds) Application and Theory of Petri Nets and Concurrency: 40th International Conference, PETRI NETS 2019, Aachen, Germany, June 23\u201328, 2019, Proceedings. Springer International Publishing, Cham, pp 365\u2013385. https:\/\/doi.org\/10.1007\/978-3-030-21571-2_20"},{"key":"469_CR21","doi-asserted-by":"crossref","unstructured":"Bozzelli L, Ganty P (2011) Complexity analysis of the backward coverability algorithm for VASS. In: RP. Lecture Notes in Computer Science, 96\u2013109. Springer","DOI":"10.1007\/978-3-642-24288-5_10"},{"key":"469_CR22","doi-asserted-by":"crossref","unstructured":"Pnueli A, Xu J, Zuck LD (2002) Liveness with (0, 1, infty)-counter abstraction. In: CAV. Lecture Notes in Computer Science, 107\u2013122. Springer","DOI":"10.1007\/3-540-45657-0_9"},{"issue":"3","key":"469_CR23","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1023\/A:1011254632723","volume":"19","author":"O Kupferman","year":"2001","unstructured":"Kupferman O, Vardi MY (2001) Model checking of safety properties. Formal Methods Syst Des 19(3):291\u2013314. https:\/\/doi.org\/10.1023\/A:1011254632723","journal-title":"Formal Methods Syst Des"},{"key":"469_CR24","unstructured":"Baier C, Katoen J-P (2008) Principles of Model Checking vol. 26202649. MIT press Cambridge"},{"key":"469_CR25","doi-asserted-by":"publisher","unstructured":"Delzanno G, Sangnier A, Zavattaro G (2010) Parameterized verification of ad hoc networks. In: CONCUR. LNCS. Springer. https:\/\/doi.org\/10.1007\/978-3-642-15375-4_22","DOI":"10.1007\/978-3-642-15375-4_22"},{"key":"469_CR26","doi-asserted-by":"crossref","unstructured":"Delzanno G, Sangnier A, Zavattaro G (2012) Verification of ad hoc networks with node and communication failures. In: FMOODS\/FORTE. Lecture Notes in Computer Science. Springer","DOI":"10.1007\/978-3-642-30793-5_15"},{"key":"469_CR27","doi-asserted-by":"crossref","unstructured":"Leroux J (2021) The reachability problem for petri nets is not primitive recursive. In: FOCS, 1241\u20131252. IEEE","DOI":"10.1109\/FOCS52979.2021.00121"},{"key":"469_CR28","doi-asserted-by":"publisher","unstructured":"Bloem R, Jacobs S, Khalimov A, Konnov I, Rubin S, Veith H, Widder J (2015) Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan and Claypool Publishers. https:\/\/doi.org\/10.2200\/S00658ED1V01Y201508DCT013","DOI":"10.2200\/S00658ED1V01Y201508DCT013"},{"key":"469_CR29","doi-asserted-by":"crossref","unstructured":"Schmitz S, Schnoebelen P (2013) The power of well-structured systems. In: CONCUR. Lecture Notes in Computer Science, 8052, 5\u201324. Springer","DOI":"10.1007\/978-3-642-40184-8_2"},{"key":"469_CR30","doi-asserted-by":"crossref","unstructured":"Blondin M, Raskin M (2020) The complexity of reachability in affine vector addition systems with states. In: Proceedings of the 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, 224\u2013236","DOI":"10.1145\/3373718.3394741"},{"key":"469_CR31","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/3-540-46002-0_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"G Delzanno","year":"2002","unstructured":"Delzanno G, Raskin J-F, Van Begin L (2002) Towards the Automated Verification of Multithreaded Java Programs. In: Katoen J-P, Stevens P (eds) Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 173\u2013187. https:\/\/doi.org\/10.1007\/3-540-46002-0_13"},{"issue":"OOPSLA","key":"469_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3485534","volume":"5","author":"N Jaber","year":"2021","unstructured":"Jaber N, Wagner C, Jacobs S, Kulkarni M, Samanta R (2021) QuickSilver: modeling and parameterized verification for distributed agreement-based systems. Proc ACM on Program Lang 5(OOPSLA):1\u201331. https:\/\/doi.org\/10.1145\/3485534","journal-title":"Proc ACM on Program Lang"},{"key":"469_CR33","unstructured":"Burrows M (2006) The chubby lock service for loosely-coupled distributed systems. In: OSDI, 335\u2013350. USENIX Association"},{"key":"469_CR34","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-540-76627-8_7","volume-title":"Stabilization, Safety, and Security of Distributed Systems","author":"D Canepa","year":"2007","unstructured":"Canepa D, Potop-Butucaru MG (2007) Stabilizing Flocking Via Leader Election in Robot Networks. In: Masuzawa T, Tixeuil S (eds) Stabilization, Safety, and Security of Distributed Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 52\u201366. https:\/\/doi.org\/10.1007\/978-3-540-76627-8_7"},{"issue":"6","key":"469_CR35","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1049\/iet-wss.2015.0030","volume":"6","author":"C Chang","year":"2016","unstructured":"Chang C, Tsai J (2016) Distributed collaborative surveillance system based on leader election protocols. IET Wirel Sens Syst 6(6):198\u2013205","journal-title":"IET Wirel Sens Syst"},{"key":"469_CR36","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-540-39724-3_22","volume-title":"Correct Hardware Design and Verification Methods","author":"EA Emerson","year":"2003","unstructured":"Emerson EA, Kahlon V (2003) Exact and Efficient Verification of Parameterized Cache Coherence Protocols. In: Geist D, Tronci E (eds) Correct Hardware Design and Verification Methods. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 247\u2013262. https:\/\/doi.org\/10.1007\/978-3-540-39724-3_22"},{"key":"469_CR37","doi-asserted-by":"crossref","unstructured":"Demsky B, Rinard M (2003) Automatic detection and repair of errors in data structures. In: Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA\u201903), 78\u201395","DOI":"10.1145\/949305.949314"},{"key":"469_CR38","doi-asserted-by":"publisher","first-page":"358","DOI":"10.1007\/11817963_33","volume-title":"Computer Aided Verification","author":"A Griesmayer","year":"2006","unstructured":"Griesmayer A, Bloem R, Cook B (2006) Repair of Boolean Programs with an Application to C. In: Ball T, Jones RB (eds) Computer Aided Verification. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 358\u2013371. https:\/\/doi.org\/10.1007\/11817963_33"},{"key":"469_CR39","doi-asserted-by":"crossref","unstructured":"Forrest S, Nguyen T, Weimer W, Goues CL (2009) A genetic programming approach to automated software repair. In: Genetic and Evolutionary Computation Conference (GECCO\u201909), 947\u2013954. ACM","DOI":"10.1145\/1569901.1570031"},{"issue":"1","key":"469_CR40","first-page":"17","volume":"51","author":"M Monperrus","year":"2018","unstructured":"Monperrus M (2018) Automatic software repair: a bibliography. ACM Comput Surv 51(1):17\u201311724","journal-title":"ACM Comput Surv"},{"issue":"5\u20136","key":"469_CR41","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner B, Schewe S (2013) Bounded synthesis. STTT 15(5\u20136):519\u2013539. https:\/\/doi.org\/10.1007\/s10009-012-0228-z","journal-title":"STTT"},{"key":"469_CR42","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1145\/3371122","volume":"4","author":"S Bansal","year":"2020","unstructured":"Bansal S, Namjoshi KS, Sa\u2019ar Y (2020) Synthesis of coordination programs from linear temporal specifications. Proc ACM Program Lang 4:54\u201315427. https:\/\/doi.org\/10.1145\/3371122","journal-title":"Proc ACM Program Lang"},{"key":"469_CR43","doi-asserted-by":"crossref","unstructured":"Vechev M, Yahav E, Yorsh G (2010) Abstraction-guided synthesis of synchronization. In: Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 327\u2013338","DOI":"10.1145\/1706299.1706338"},{"key":"469_CR44","doi-asserted-by":"crossref","unstructured":"Frenkel H, Grumberg O, Pasareanu C, Sheinvald S (2020) Assume, guarantee or repair. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 211\u2013227. Springer","DOI":"10.1007\/978-3-030-45190-5_12"},{"key":"469_CR45","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-27940-9_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Finkbeiner","year":"2012","unstructured":"Finkbeiner B, Jacobs S (2012) Lazy Synthesis. In: Kuncak V, Rybalchenko A (eds) Verification, Model Checking, and Abstract Interpretation. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 219\u2013234. https:\/\/doi.org\/10.1007\/978-3-642-27940-9_15"},{"key":"469_CR46","doi-asserted-by":"publisher","unstructured":"Esparza J (2014) Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In: STACS. LIPIcs, Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik. https:\/\/doi.org\/10.4230\/LIPIcs.STACS.2014.1","DOI":"10.4230\/LIPIcs.STACS.2014.1"},{"key":"469_CR47","doi-asserted-by":"crossref","unstructured":"Clarke EM, Henzinger TA, Veith H, Bloem R (2018) Handbook of Model Checking. Springer","DOI":"10.1007\/978-3-319-10575-8"},{"key":"469_CR48","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-02658-4_9","volume-title":"Computer Aided Verification","author":"G Basler","year":"2009","unstructured":"Basler G, Mazzucchi M, Wahl T, Kroening D (2009) Symbolic Counter Abstraction for Concurrent Software. In: Bouajjani A, Maler O (eds) Computer Aided Verification. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 64\u201378. https:\/\/doi.org\/10.1007\/978-3-642-02658-4_9"},{"key":"469_CR49","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-662-49122-5_23","volume-title":"Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings","author":"S Au\u00dferlechner","year":"2016","unstructured":"Au\u00dferlechner S, Jacobs S, Khalimov A (2016) Tight Cutoffs for Guarded Protocols with Fairness. In: Jobstmann B, Leino KRM (eds) Verification, Model Checking, and Abstract Interpretation: 17th International Conference, VMCAI 2016, St. Petersburg, FL, USA, January 17-19, 2016. Proceedings. Springer Berlin Heidelberg, Berlin, Heidelberg, pp 476\u2013494. https:\/\/doi.org\/10.1007\/978-3-662-49122-5_23"},{"key":"469_CR50","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/978-3-319-73721-8_12","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S Jacobs","year":"2018","unstructured":"Jacobs S, Sakr M (2018) Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity. In: Dillig I, Palsberg J (eds) Verification, Model Checking, and Abstract Interpretation. Springer International Publishing, Cham, pp 247\u2013268. https:\/\/doi.org\/10.1007\/978-3-319-73721-8_12"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00469-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-025-00469-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-025-00469-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,30]],"date-time":"2025-09-30T15:26:33Z","timestamp":1759245993000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-025-00469-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,18]]},"references-count":50,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["469"],"URL":"https:\/\/doi.org\/10.1007\/s10703-025-00469-2","relation":{"has-preprint":[{"id-type":"doi","id":"10.21203\/rs.3.rs-4635496\/v1","asserted-by":"object"}]},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,18]]},"assertion":[{"value":"25 June 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 February 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"18 April 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}