{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:02:10Z","timestamp":1776304930501,"version":"3.50.1"},"reference-count":95,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["101089343"],"award-info":[{"award-number":["101089343"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100020595","name":"National Science and Technology Council","doi-asserted-by":"publisher","award":["112-2222-E-004-001-MY3"],"award-info":[{"award-number":["112-2222-E-004-001-MY3"]}],"id":[{"id":"10.13039\/100020595","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2024,1,2]]},"abstract":"<jats:p>Verifying safety and liveness over array systems is a highly challenging problem. Array systems naturally capture parameterized systems such as distributed protocols with an unbounded number of processes. Such distributed protocols often exploit process IDs during their computation, resulting in array systems whose element values range over an infinite domain. In this paper, we develop a novel framework for proving safety and liveness over array systems. The crux of the framework is to overapproximate an array system as a string rewriting system (i.e. over a finite alphabet) by means of a new predicate abstraction that exploits the so-called indexed predicates. This allows us to tap into powerful verification methods for string rewriting systems that have been heavily developed in the last two decades or so (e.g. regular model checking). We demonstrate how our method yields simple, automatically verifiable proofs of safety and liveness properties for challenging examples, including Dijkstra\u2019s self-stabilizing protocol and the Chang-Roberts leader election protocol.<\/jats:p>","DOI":"10.1145\/3632864","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"638-666","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Regular Abstractions for Array Systems"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4064-8413","authenticated-orcid":false,"given":"Chih-Duo","family":"Hong","sequence":"first","affiliation":[{"name":"National Chengchi University, Taipei, Taiwan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4715-5096","authenticated-orcid":false,"given":"Anthony W.","family":"Lin","sequence":"additional","affiliation":[{"name":"Max-Planck Institute for Software Systems (MPI-SWS), Kaiserslautern, Germany"},{"name":"University of Kaiserslautern-Landau, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(89)90138-2"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0216-8"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_7"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-008-0062-9"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0406-x"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-011-0212-z"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_7"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_49"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2017-1458"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_23"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_9"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-45190-5_8"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_9"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/876638.876642"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/2886151"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2000.855755"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-004-1133-y"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_29"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_31"},{"key":"e_1_3_1_21_1","volume-title":"The Calculus of Computation: Decision Procedures with Applications to Verification","author":"Bradley Aaron R.","year":"1998","unstructured":"Aaron R. Bradley and Zohar Manna. 1998. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer."},{"key":"e_1_3_1_22_1","first-page":"427","volume-title":"International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)","author":"Bradley Aaron R.","year":"2006","unstructured":"Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2006. What\u2019s Decidable about Arrays?. In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer, 427\u2013442."},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/359104.359108"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102244"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_4"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-016-0257-4"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-19992-9_10"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_8"},{"key":"e_1_3_1_29_1","first-page":"126","volume-title":"International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI)","author":"Clarke Edmund","year":"2006","unstructured":"Edmund Clarke, Muralidhar Talupur, and Helmut Veith. 2006. Environment Abstraction for Parameterized Verification. In International Workshop on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer, 126\u2013141."},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_4"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/10590.10611"},{"key":"e_1_3_1_32_1","volume-title":"Model Checking","author":"Clarke Edmund M.","year":"2018","unstructured":"Edmund M. Clarke Jr, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. 2018. Model Checking. MIT press."},{"issue":"2","key":"e_1_3_1_33_1","article-title":"Transforming Structures by Set Interpretations","volume":"3","author":"Colcombet Thomas","year":"2007","unstructured":"Thomas Colcombet and Christof L\u00f6ding. 2007. Transforming Structures by Set Interpretations. Logical Methods in Computer Science (LMCS) 3, 2 (2007), paper-4.","journal-title":"Logical Methods in Computer Science (LMCS)"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250771"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_15"},{"key":"e_1_3_1_37_1","first-page":"337","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"Mendon\u00e7a de Moura Leonardo","year":"2008","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 337\u2013340."},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139236119"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-5695-3_7"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_28"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0155-3"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_10"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054103001881"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_14"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935310"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-69322-0_17"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54577-5_24"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503291"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-015-0411-0"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/146637.146681"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71995-1_14"},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950330"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_15"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_39"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00018-X"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_36"},{"key":"e_1_3_1_59_1","volume-title":"Symbolic techniques for parameterised verification","author":"Hong Chih-Duo","year":"2022","unstructured":"Chih-Duo Hong. 2022. Symbolic techniques for parameterised verification. Ph.D. Dissertation. University of Oxford."},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_23"},{"key":"e_1_3_1_61_1","doi-asserted-by":"crossref","first-page":"447","DOI":"10.1007\/978-3-319-10575-8_15","volume-title":"Handbook of Model Checking","author":"Jhala Ranjit","year":"2018","unstructured":"Ranjit Jhala, Andreas Podelski, and Andrey Rybalchenko. 2018. Predicate Abstraction for Program Verification: Safety and Termination. In Handbook of Model Checking. Springer, 447\u2013491."},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.03.003"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2017.04.009"},{"key":"e_1_3_1_64_1","volume-title":"Mona Version 1.4: User Manual","author":"Klarlund Nils","year":"2001","unstructured":"Nils Klarlund and Anders M\u00f8ller. 2001. Mona Version 1.4: User Manual. BRICS, Department of Computer Science, University of Aarhus Denmark."},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1142\/S012905410200128X"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2015.7542257"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.5555\/3086916"},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24622-0_22"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-27813-9_11"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297658.1297662"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-015-9183-0"},{"key":"e_1_3_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41540-6_7"},{"key":"e_1_3_1_73_1","first-page":"97","volume-title":"Model Checking, Synthesis, and Learning: Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday","author":"Lin Anthony W.","year":"2022","unstructured":"Anthony W. Lin and Philipp R\u00fcmmer. 2022. Regular model checking revisited. In Model Checking, Synthesis, and Learning: Essays Dedicated to Bengt Jonsson on The Occasion of His 60th Birthday. Springer, 97\u2013114."},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341301.3359651"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74061-2_14"},{"key":"e_1_3_1_76_1","first-page":"131","article-title":"Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays","volume":"18","author":"Mann Makai","year":"2022","unstructured":"Makai Mann, Ahmed Irfan, Alberto Griggio, Oded Padon, and Clark Barrett. 2022. Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays. Logical Methods in Computer Science (LMCS) 18 (2022), 131\u2013147.","journal-title":"Logical Methods in Computer Science (LMCS)"},{"key":"e_1_3_1_77_1","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Manna Zohar","year":"2012","unstructured":"Zohar Manna and Amir Pnueli. 2012. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Science & Business Media."},{"issue":"1","key":"e_1_3_1_78_1","doi-asserted-by":"crossref","first-page":"35","DOI":"10.1007\/978-94-011-1793-7_2","article-title":"Towards a mathematical science of computation","volume":"1","author":"McCarthy John","year":"1993","unstructured":"John McCarthy. 1993. Towards a mathematical science of computation. Program Verification: Fundamental Issues in Computer Science 1, 1 (1993), 35\u201356.","journal-title":"Program Verification: Fundamental Issues in Computer Science"},{"key":"e_1_3_1_79_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_31"},{"key":"e_1_3_1_80_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_11"},{"key":"e_1_3_1_81_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-99725-4_4"},{"key":"e_1_3_1_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53291-8_12"},{"key":"e_1_3_1_83_1","first-page":"1","volume-title":"Symposium on Principles of Programming Languages (POPL)","author":"Padon Oded","year":"2017","unstructured":"Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. 2017. Reducing Liveness to Safety in First-Order Logic. Symposium on Principles of Programming Languages (POPL) 2, POPL (2017), 1\u201333."},{"key":"e_1_3_1_84_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-021-00377-1"},{"key":"e_1_3_1_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-021-00370-8"},{"key":"e_1_3_1_86_1","first-page":"1","article-title":"Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification","volume":"60","author":"Pani Thomas","year":"2023","unstructured":"Thomas Pani, Georg Weissenbacher, and Florian Zuleger. 2023. Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification. Formal Methods in System Design (FMSD) 60 (2023), 1\u201338.","journal-title":"Formal Methods in System Design (FMSD)"},{"key":"e_1_3_1_87_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_6"},{"key":"e_1_3_1_88_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28756-5_17"},{"issue":"4","key":"e_1_3_1_89_1","first-page":"25","article-title":"Backward Reachability of Array-Based Systems by SMT Solving: Termination and Invariant Synthesis","volume":"6","author":"Ranise Silvio","year":"2010","unstructured":"Silvio Ranise and Silvio Ghilardi. 2010. Backward Reachability of Array-Based Systems by SMT Solving: Termination and Invariant Synthesis. Logical Methods in Computer Science (LMCS) 6, 4 (2010), 25\u201344.","journal-title":"Logical Methods in Computer Science (LMCS)"},{"key":"e_1_3_1_90_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.11.018"},{"key":"e_1_3_1_91_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_3"},{"key":"e_1_3_1_92_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_7"},{"key":"e_1_3_1_93_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192414"},{"key":"e_1_3_1_94_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02962-6"},{"key":"e_1_3_1_95_1","first-page":"322","volume-title":"Symposium on Logic in Computer Science (LICS)","author":"Vardi Moshe Y.","year":"1986","unstructured":"Moshe Y. Vardi and Pierre Wolper. 1986. An Automata-Theoretic Approach to Automatic Program Verification. In Symposium on Logic in Computer Science (LICS). IEEE, 322\u2013331."},{"key":"e_1_3_1_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/3395363.3397378"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632864","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632864","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:03:04Z","timestamp":1751659384000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632864"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":95,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632864"],"URL":"https:\/\/doi.org\/10.1145\/3632864","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}