{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:26:15Z","timestamp":1740122775269,"version":"3.37.3"},"reference-count":74,"publisher":"Springer Science and Business Media LLC","issue":"1-3","license":[{"start":{"date-parts":[[2023,10,6]],"date-time":"2023-10-06T00:00:00Z","timestamp":1696550400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,10,6]],"date-time":"2023-10-06T00:00:00Z","timestamp":1696550400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"TU Wien"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2024,12]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Parameterized programs are composed of an arbitrary number of concurrent, infinite-state threads. Automated safety and liveness proofs of such parameterized software are hard; state-of-the-art methods for their formal verification rely on intricate abstractions and complicated proof techniques that impede automation. In this paper, we introduce <jats:italic>thread-modular counter abstraction<\/jats:italic> (TMCA), a lean new abstraction technique to replace the existing heavy proof machinery. TMCA is a structured abstraction framework built from a novel combination of <jats:italic>counter abstraction<\/jats:italic>, <jats:italic>thread-modular reasoning<\/jats:italic>, and <jats:italic>predicate abstraction<\/jats:italic>. Its major strength lies in reducing the parameterized verification problem to the sequential setting, for which powerful proof procedures, efficient heuristics, and effective automated tools have been developed over the past decades. In this work, we first introduce the TMCA abstraction paradigm, then present a fully automated method for parameterized safety proofs, and finally discuss its application to automated termination and liveness proofs of parameterized software.<\/jats:p>","DOI":"10.1007\/s10703-023-00439-6","type":"journal-article","created":{"date-parts":[[2023,10,6]],"date-time":"2023-10-06T15:01:41Z","timestamp":1696604501000},"page":"108-145","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification"],"prefix":"10.1007","volume":"64","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4434-0248","authenticated-orcid":false,"given":"Thomas","family":"Pani","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Georg","family":"Weissenbacher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,10,6]]},"reference":[{"key":"439_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Chen Y, Delzanno G, Haziza F, Hong C, Rezine A (2010) Constrained monotonic abstraction: a CEGAR for parameterized verification. In: CONCUR, Lecture notes in computer science, vol 6269. Springer, Berlin, pp 86\u2013101","DOI":"10.1007\/978-3-642-15375-4_7"},{"issue":"1\u20132","key":"439_CR2","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1999.2843","volume":"160","author":"PA Abdulla","year":"2000","unstructured":"Abdulla PA, Cerans K, Jonsson B, Tsay Y (2000) Algorithmic analysis of programs with well quasi-ordered domains. Inf Comput 160(1\u20132):109\u2013127","journal-title":"Inf Comput"},{"key":"439_CR3","doi-asserted-by":"crossref","unstructured":"Albert E, Arenas P, Flores-Montoya A, Genaim S, G\u00f3mez-Zamalloa M, Martin-Martin E, Puebla G, Rom\u00e1n-D\u00edez G (2014) SACO: static analyzer for concurrent objects. In: TACAS, Lecture notes in computer science, vol 8413. Springer, Berlin, pp 562\u2013567","DOI":"10.1007\/978-3-642-54862-8_46"},{"key":"439_CR4","doi-asserted-by":"crossref","unstructured":"Albert E, Flores-Montoya A, Genaim S, Martin-Martin E (2013) Termination and cost analysis of loops with concurrent interleavings. In: ATVA, Lecture notes in computer science, vol 8172. Springer, Berlin, pp 349\u2013364","DOI":"10.1007\/978-3-319-02444-8_25"},{"key":"439_CR5","doi-asserted-by":"crossref","unstructured":"Alberti F, Bruttomesso R, Ghilardi S, Ranise S, Sharygina N (2012) Lazy abstraction with interpolants for arrays. In: LPAR, Lecture notes in computer science, vol 7180. Springer, Berlin, pp 46\u201361","DOI":"10.1007\/978-3-642-28717-6_7"},{"key":"439_CR6","doi-asserted-by":"crossref","unstructured":"Alur R, Bod\u00edk R, Juniwal G, Martin MMK, Raghothaman M, Seshia SA, Singh R, Solar-Lezama A, Torlak E, Udupa A (2013) Syntax-guided synthesis. In: FMCAD. IEEE, pp 1\u20138","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"439_CR7","doi-asserted-by":"crossref","unstructured":"Aminof B, Rubin S, Stoilkovska I, Widder J, Zuleger F (2018) Parameterized model checking of synchronous distributed algorithms by abstraction. In: VMCAI, Lecture notes in computer science, vol 10747. Springer, Berlin, pp 1\u201324","DOI":"10.1007\/978-3-319-73721-8_1"},{"key":"439_CR8","doi-asserted-by":"crossref","unstructured":"Apt KR, de\u00a0Boer FS, Olderog E (2009) Verification of sequential and concurrent programs. Texts in Computer Science. Springer, Berlin","DOI":"10.1007\/978-1-84882-745-5"},{"key":"439_CR9","doi-asserted-by":"crossref","unstructured":"Arons T, Pnueli A, Ruah S, Xu J, Zuck LD (2001) Parameterized verification with automatically computed inductive assertions. In: CAV, Lecture notes in computer science, vol 2102. Springer, Berlin, pp 221\u2013234","DOI":"10.1007\/3-540-44585-4_19"},{"key":"439_CR10","doi-asserted-by":"crossref","unstructured":"Ball T, Podelski A, Rajamani SK (2001) Boolean and cartesian abstraction for model checking C programs. In: TACAS, Lecture notes in computer science, vol 2031. Springer, Berlin, pp 268\u2013283","DOI":"10.1007\/3-540-45319-9_19"},{"key":"439_CR11","unstructured":"Benchmarks (2022) https:\/\/github.com\/thpani\/eldarica\/tree\/tmca\/regression-tests\/environment-abstract"},{"key":"439_CR12","doi-asserted-by":"crossref","unstructured":"Beyer D (2020) Advances in automatic software verification: SV-COMP 2020. In: TACAS (2), Lecture notes in computer science, vol 12079. Springer, Berlin, pp 347\u2013367","DOI":"10.1007\/978-3-030-45237-7_21"},{"key":"439_CR13","doi-asserted-by":"crossref","unstructured":"Beyer D, L\u00f6we S, Wendler P (2015) Refinement selection. In: SPIN, Lecture notes in computer science, vol 9232. Springer, Berlin, pp 20\u201338","DOI":"10.1007\/978-3-319-23404-5_3"},{"key":"439_CR14","doi-asserted-by":"crossref","unstructured":"Brockschmidt M, Cook B, Fuhs C (2013) Better termination proving through cooperation. In: CAV, Lecture notes in computer science, vol 8044. Springer, Berlin, pp 413\u2013429","DOI":"10.1007\/978-3-642-39799-8_28"},{"key":"439_CR15","doi-asserted-by":"crossref","unstructured":"Cook B, Gotsman A, Podelski A, Rybalchenko A, Vardi MY (2007) Proving that programs eventually do something good. In: POPL. ACM, pp 265\u2013276","DOI":"10.1145\/1190216.1190257"},{"key":"439_CR16","doi-asserted-by":"crossref","unstructured":"Cook B, Podelski A, Rybalchenko A (2005) Abstraction refinement for termination. In: SAS, Lecture notes in computer science, vol 3672. Springer, Berlin, pp 87\u2013101","DOI":"10.1007\/11547662_8"},{"key":"439_CR17","doi-asserted-by":"crossref","unstructured":"Cook B, Podelski A, Rybalchenko A (2006) Termination proofs for systems code. In: PLDI. ACM, pp 415\u2013426","DOI":"10.1145\/1133981.1134029"},{"key":"439_CR18","doi-asserted-by":"crossref","unstructured":"Cook B, Podelski A, Rybalchenko A (2007) Proving thread termination. In: PLDI. ACM, pp 320\u2013330","DOI":"10.1145\/1250734.1250771"},{"key":"439_CR19","doi-asserted-by":"crossref","unstructured":"Cook B, See A, Zuleger F (2013) Ramsey vs. lexicographic termination proving. In: TACAS, Lecture notes in computer science, vol 7795. Springer, Berlin, pp 47\u201361","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"439_CR20","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura LM, Bj\u00f8rner N (2008) Z3: an efficient SMT solver. In: TACAS, Lecture notes in computer science, vol 4963. Springer, Berlin, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"439_CR21","doi-asserted-by":"crossref","unstructured":"Donaldson AF, Kaiser A, Kroening D, Wahl T (2011) Symmetry-aware predicate abstraction for shared-variable concurrent programs. In: CAV, Lecture notes in computer science, vol 6806. Springer, Berlin, pp 356\u2013371","DOI":"10.1007\/978-3-642-22110-1_28"},{"issue":"7","key":"439_CR22","doi-asserted-by":"publisher","first-page":"1165","DOI":"10.1109\/TCAD.2008.923410","volume":"27","author":"V D\u2019Silva","year":"2008","unstructured":"D\u2019Silva V, Kroening D, Weissenbacher G (2008) A survey of automated techniques for formal software verification. IEEE Trans Comput Aided Des Integr Circuits Syst 27(7), 1165\u20131178","journal-title":"IEEE Trans Comput Aided Des Integr Circuits Syst"},{"key":"439_CR23","unstructured":"ELDARICA with TMCA (2020) https:\/\/github.com\/thpani\/eldarica\/tree\/tmca"},{"key":"439_CR24","unstructured":"Falke S, Kapur D, Sinz C (2011) Termination analysis of C programs using compiler intermediate languages. In: RTA, LIPIcs, vol\u00a010. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, pp 41\u201350"},{"key":"439_CR25","doi-asserted-by":"crossref","unstructured":"Farzan A, Kincaid Z, Podelski A (2014) Proofs that count. In: POPL. ACM, pp 151\u2013164","DOI":"10.1145\/2535838.2535885"},{"key":"439_CR26","doi-asserted-by":"crossref","unstructured":"Farzan A, Kincaid Z, Podelski A (2015) Proof spaces for unbounded parallelism. In: POPL. ACM, pp 407\u2013420","DOI":"10.1145\/2676726.2677012"},{"key":"439_CR27","doi-asserted-by":"crossref","unstructured":"Farzan A, Kincaid Z, Podelski A (2016) Proving liveness of parameterized programs. In: LICS. ACM, pp 185\u2013196","DOI":"10.1145\/2933575.2935310"},{"issue":"1\u20132","key":"439_CR28","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! Theor Comput Sci 256(1\u20132):63\u201392","journal-title":"Theor Comput Sci"},{"key":"439_CR29","doi-asserted-by":"crossref","unstructured":"Flanagan C, Qadeer S (2003) Thread-modular model checking. In: SPIN, Lecture notes in computer science, vol 2648. Springer, Berlin, pp 213\u2013224","DOI":"10.1007\/3-540-44829-2_14"},{"issue":"5","key":"439_CR30","first-page":"517","volume":"18","author":"Z Ganjei","year":"2016","unstructured":"Ganjei Z, Rezine A, Eles P, Peng Z (2016) Counting dynamically synchronizing processes. STTT 18(5):517\u2013534","journal-title":"Counting dynamically synchronizing processes. STTT"},{"key":"439_CR31","doi-asserted-by":"crossref","unstructured":"Ganjei Z, Rezine A, Eles P, Peng Z (2015) Abstracting and counting synchronizing processes. In: VMCAI, Lecture notes in computer science, vol 8931. Springer, Berlin, pp 227\u2013244","DOI":"10.1007\/978-3-662-46081-8_13"},{"key":"439_CR32","doi-asserted-by":"crossref","unstructured":"Ghilardi S, Nicolini E, Ranise S, Zucchelli D (2008) Towards SMT model checking of array-based systems. In: IJCAR, Lecture notes in computer science, vol 5195. Springer, Berlin, pp 67\u201382","DOI":"10.1007\/978-3-540-71070-7_6"},{"key":"439_CR33","doi-asserted-by":"crossref","unstructured":"Ghilardi S, Ranise S (2010) Backward reachability of array-based systems by SMT solving: Termination and invariant synthesis. Log Methods Comput Sci 6(4)","DOI":"10.2168\/LMCS-6(4:10)2010"},{"key":"439_CR34","doi-asserted-by":"crossref","unstructured":"Giesl J, Brockschmidt M, Emmes F, Frohn F, Fuhs C, Otto C, Pl\u00fccker M, Schneider-Kamp P, Str\u00f6der T, Swiderski S, Thiemann R (2014) Proving termination of programs automatically with aprove. In: IJCAR, Lecture notes in computer science, vol 8562. Springer, Berlin, pp 184\u2013191","DOI":"10.1007\/978-3-319-08587-6_13"},{"key":"439_CR35","doi-asserted-by":"crossref","unstructured":"Graf S, Sa\u00efdi H (1997) Construction of abstract state graphs with PVS. In: CAV, Lecture notes in computer science, vol 1254. Springer, Berlin, pp 72\u201383","DOI":"10.1007\/3-540-63166-6_10"},{"key":"439_CR36","doi-asserted-by":"crossref","unstructured":"Grebenshchikov S, Lopes NP, Popeea C, Rybalchenko A (2012) Synthesizing software verifiers from proof rules. In: PLDI. ACM, pp 405\u2013416","DOI":"10.1145\/2254064.2254112"},{"key":"439_CR37","doi-asserted-by":"crossref","unstructured":"Gulwani S, Zuleger F (2010) The reachability-bound problem. In: PLDI. ACM, pp 292\u2013304","DOI":"10.1145\/1806596.1806630"},{"key":"439_CR38","doi-asserted-by":"crossref","unstructured":"Gurfinkel A, Shoham S, Meshman Y (2016) Smt-based verification of parameterized systems. In: SIGSOFT FSE. ACM, pp 338\u2013348","DOI":"10.1145\/2950290.2950330"},{"key":"439_CR39","doi-asserted-by":"crossref","unstructured":"Heizmann M, Hoenicke J, Podelski A (2013) Software model checking for people who love automata. In: CAV, Lecture notes in computer science, vol 8044. Springer, Berlin, pp 36\u201352","DOI":"10.1007\/978-3-642-39799-8_2"},{"key":"439_CR40","doi-asserted-by":"crossref","unstructured":"Henzinger TA, Jhala R, Majumdar R, Qadeer S (2003) Thread-modular abstraction refinement. In: CAV, Lecture notes in computer science, vol 2725. Springer, Berlin, pp 262\u2013274","DOI":"10.1007\/978-3-540-45069-6_27"},{"key":"439_CR41","volume-title":"The art of multiprocessor programming","author":"M Herlihy","year":"2008","unstructured":"Herlihy M, Shavit N (2008) The art of multiprocessor programming. Morgan Kaufmann, Burlington"},{"key":"439_CR42","doi-asserted-by":"crossref","unstructured":"Hoenicke J, Majumdar R, Podelski A (2017) Thread modularity at many levels: a pearl in compositional verification. In: POPL. ACM, pp 473\u2013485","DOI":"10.1145\/3009837.3009893"},{"key":"439_CR43","doi-asserted-by":"crossref","unstructured":"Hojjat H, R\u00fcmmer P (2018) The ELDARICA horn solver. In: FMCAD. IEEE, pp 1\u20137","DOI":"10.23919\/FMCAD.2018.8603013"},{"key":"439_CR44","doi-asserted-by":"crossref","unstructured":"Hojjat H, R\u00fcmmer P, Subotic P, Yi W (2014) Horn clauses for communicating timed systems. In: HCVS, vol 169. EPTCS, pp 39\u201352","DOI":"10.4204\/EPTCS.169.6"},{"issue":"4","key":"439_CR45","doi-asserted-by":"publisher","first-page":"21:1","DOI":"10.1145\/1592434.1592438","volume":"41","author":"R Jhala","year":"2009","unstructured":"Jhala R, Majumdar R (2009) Software model checking. ACM Comput Surv 41(4):21:1\u201321:54","journal-title":"ACM Comput Surv"},{"key":"439_CR46","doi-asserted-by":"crossref","unstructured":"John A, Konnov I, Schmid U, Veith H, Widder J (2013) Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: FMCAD. IEEE, pp 201\u2013209","DOI":"10.1109\/FMCAD.2013.6679411"},{"key":"439_CR47","unstructured":"Jones CB (1983) Specification and design of (parallel) programs. In: IFIP Congress. North-Holland\/IFIP, pp 321\u2013332"},{"key":"439_CR48","doi-asserted-by":"crossref","unstructured":"Kaiser A, Kroening D, Wahl T (2010) Dynamic cutoff detection in parameterized concurrent programs. In: CAV, Lecture notes in computer science, vol 6174. Springer, Berlin, pp 645\u2013659","DOI":"10.1007\/978-3-642-14295-6_55"},{"key":"439_CR49","doi-asserted-by":"crossref","unstructured":"Kaiser A, Kroening D, Wahl T (2014) Lost in abstraction: monotonicity in multi-threaded programs. In: CONCUR, Lecture notes in computer science, vol 8704. Springer, Berlin, pp 141\u2013155","DOI":"10.1007\/978-3-662-44584-6_11"},{"key":"439_CR50","doi-asserted-by":"crossref","unstructured":"La Torre S, Madhusudan P, Parlato G (2010) Model-checking parameterized concurrent programs using linear interfaces. In: CAV, Lecture notes in computer science, vol 6174. Springer, Berlin, pp 629\u2013644","DOI":"10.1007\/978-3-642-14295-6_54"},{"issue":"4","key":"439_CR51","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/s00236-015-0236-z","volume":"53","author":"J Leroux","year":"2016","unstructured":"Leroux J, R\u00fcmmer P, Subotic P (2016) Guiding craig interpolation with domain-specific abstractions. Acta Inf 53(4):387\u2013424","journal-title":"Acta Inf"},{"key":"439_CR52","doi-asserted-by":"crossref","unstructured":"McMillan KL (2006) Lazy abstraction with interpolants. In: CAV, Lecture notes in computer science, vol 4144. Springer, Berlin, pp 123\u2013136","DOI":"10.1007\/11817963_14"},{"key":"439_CR53","doi-asserted-by":"crossref","unstructured":"Min\u00e9 A (2011) Static analysis of run-time errors in embedded critical parallel C programs. In: ESOP, Lecture notes in computer science, vol 6602. Springer, Berlin, pp 398\u2013418","DOI":"10.1007\/978-3-642-19718-5_21"},{"key":"439_CR54","unstructured":"Nieto LP (2001) Completeness of the owicki-gries system for parameterized parallel programs. In: IPDPS. IEEE Computer Society, p 150"},{"key":"439_CR55","unstructured":"Owicki SS (1975) Axiomatic proof techniques for parallel programs. Ph.D. thesis, Cornell University"},{"key":"439_CR56","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"SS Owicki","year":"1976","unstructured":"Owicki SS, Gries D (1976) An axiomatic proof technique for parallel programs I. Acta Inf 6:319\u2013340","journal-title":"Acta Inf"},{"key":"439_CR57","unstructured":"Pacman (2022) https:\/\/gitlab.liu.se\/live\/pacman"},{"key":"439_CR58","doi-asserted-by":"publisher","first-page":"26:1","DOI":"10.1145\/3158114","volume":"2","author":"O Padon","year":"2018","unstructured":"Padon O, Hoenicke J, Losa G, Podelski A, Sagiv M, Shoham S (2018) Reducing liveness to safety in first-order logic. Proc ACM Program Lang 2:26:1\u201326:33","journal-title":"Proc ACM Program Lang"},{"key":"439_CR59","doi-asserted-by":"crossref","unstructured":"Pani T, Weissenbacher G, Zuleger F (2018) Rely-guarantee reasoning for automated bound analysis of lock-free algorithms. In: FMCAD. IEEE, pp 1\u20139","DOI":"10.23919\/FMCAD.2018.8603020"},{"key":"439_CR60","unstructured":"Pani T, Weissenbacher G, Zuleger F (2020) Thread-modular counter abstraction for parameterized program safety. In: FMCAD. IEEE, pp 67\u201376"},{"key":"439_CR61","doi-asserted-by":"crossref","unstructured":"Petrank E, Musuvathi M, Steensgaard B (2009) Progress guarantee for parallel programs via bounded lock-freedom. In: PLDI. ACM, pp 144\u2013154","DOI":"10.1145\/1542476.1542493"},{"key":"439_CR62","doi-asserted-by":"crossref","unstructured":"Pnueli A, Ruah S, Zuck LD (2001) Automatic deductive verification with invisible invariants. In: TACAS, Lecture notes in computer science, vol 2031. Springer, pp 82\u201397","DOI":"10.1007\/3-540-45319-9_7"},{"key":"439_CR63","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, vol 2404. Springer, Berlin, pp 107\u2013122","DOI":"10.1007\/3-540-45657-0_9"},{"key":"439_CR64","doi-asserted-by":"crossref","unstructured":"Podelski A, Rybalchenko A (2004) Transition invariants. In: LICS. IEEE computer society, pp 32\u201341","DOI":"10.1109\/LICS.2004.1319598"},{"key":"439_CR65","doi-asserted-by":"crossref","unstructured":"Podelski A, Rybalchenko A (2005) Transition predicate abstraction and fair termination. In: POPL. ACM, pp 132\u2013144","DOI":"10.1145\/1040305.1040317"},{"key":"439_CR66","doi-asserted-by":"crossref","unstructured":"Popeea C, Rybalchenko A (2012) Compositional termination proofs for multi-threaded programs. In: TACAS, Lecture notes in computer science, vol 7214. Springer, Berlin, pp 237\u2013251","DOI":"10.1007\/978-3-642-28756-5_17"},{"key":"439_CR67","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer P (2008) A constraint sequent calculus for first-order logic with linear integer arithmetic. In: LPAR, Lecture notes in computer science, vol 5330. Springer, Berlin, pp 274\u2013289","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"439_CR68","doi-asserted-by":"crossref","unstructured":"R\u00fcmmer P, Subotic P (2013) Exploring interpolants. In: FMCAD. IEEE, pp 69\u201376","DOI":"10.1109\/FMCAD.2013.6679393"},{"key":"439_CR69","doi-asserted-by":"crossref","unstructured":"S\u00e1nchez A, Sankaranarayanan S, S\u00e1nchez C, Chang BE (2012) Invariant generation for parametrized systems using self-reflection - (extended version). In: SAS, Lecture notes in computer science, vol 7460. Springer, Berlin, pp 146\u2013163","DOI":"10.1007\/978-3-642-33125-1_12"},{"key":"439_CR70","doi-asserted-by":"crossref","unstructured":"Vafeiadis V (2010) Rgsep action inference. In: VMCAI, Lecture Notes in Computer Science, vol 5944. Springer, Berlin, pp 345\u2013361","DOI":"10.1007\/978-3-642-11319-2_25"},{"key":"439_CR71","unstructured":"Vardi MY, Wolper P (1986) An automata-theoretic approach to automatic program verification (preliminary report). In: LICS. IEEE Computer Society, pp 332\u2013344"},{"issue":"1\u20132","key":"439_CR72","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0168-0072(91)90066-U","volume":"51","author":"MY Vardi","year":"1991","unstructured":"Vardi MY (1991) Verification of concurrent programs: the automata-theoretic framework. Ann Pure Appl Log 51(1\u20132):79\u201398","journal-title":"Ann Pure Appl Log"},{"key":"439_CR73","unstructured":"Wickerson J (2011) RGSep https:\/\/johnwickerson.github.io\/talks\/rely_guarantee.pdf. Imperial College lectures on Rely-Guarantee Separation Logic"},{"issue":"3\u20134","key":"439_CR74","first-page":"139","volume":"30","author":"LD Zuck","year":"2004","unstructured":"Zuck LD, Pnueli A (2004) Model checking and abstraction to the aid of parameterized systems (a survey). Comput Lang Syst Struct 30(3\u20134):139\u2013169","journal-title":"Comput Lang Syst Struct"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00439-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10703-023-00439-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-023-00439-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,28]],"date-time":"2024-12-28T18:03:11Z","timestamp":1735408991000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10703-023-00439-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,6]]},"references-count":74,"journal-issue":{"issue":"1-3","published-print":{"date-parts":[[2024,12]]}},"alternative-id":["439"],"URL":"https:\/\/doi.org\/10.1007\/s10703-023-00439-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2023,10,6]]},"assertion":[{"value":"16 March 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 August 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"6 October 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}