Regular Abstractions for Array Systems
Article No.: 22, Pages 638 - 666
Abstract
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's self-stabilizing protocol and the Chang-Roberts leader election protocol.
References
[1]
Martin Abadi. 1989. The power of temporal proofs. Theoretical Computer Science, 65, 1 (1989), 35–83.
[2]
Parosh Aziz Abdulla. 2012. Regular Model Checking. International Journal on Software Tools for Technology Transfer (STTT), 14, 2 (2012), 109–118.
[3]
Parosh Aziz Abdulla, Yu-Fang Chen, Giorgio Delzanno, Frédéric Haziza, Chih-Duo Hong, and Ahmed Rezine. 2010. Constrained Monotonic Abstraction: A CEGAR for Parameterized Verification. In International Conference on Concurrency Theory (CONCUR). Springer, 86–101.
[4]
Parosh Aziz Abdulla, Giorgio Delzanno, and Ahmed Rezine. 2009. Approximated Parameterized Verification of Infinite-State Processes with Global Conditions. Formal Methods in System Design (FMSD), 34, 2 (2009), 126–156.
[5]
Parosh Aziz Abdulla, Frédéric Haziza, and Lukáš Holík. 2016. Parameterized Verification Through View Abstraction. International Journal on Software Tools for Technology Transfer (STTT), 18, 5 (2016), 495–516.
[6]
Parosh Aziz Abdulla, Bengt Jonsson, Marcus Nilsson, Julien d’Orso, and Mayank Saksena. 2012. Regular Model Checking for LTL(MSO). International Journal on Software Tools for Technology Transfer (STTT), 14, 2 (2012), 223–241.
[7]
Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, and Natasha Sharygina. 2012. SAFARI: SMT-Based Abstraction for Arrays with Interpolants. In International Conference on Computer-Aided Verification (CAV). Springer, 679–685.
[8]
Francesco Alberti, Silvio Ghilardi, and Natasha Sharygina. 2017. A Framework for the Verification of Parameterized Infinite-State Systems. Fundamenta Informaticae, 150, 1 (2017), 1–24.
[9]
George Argyros and Loris D’Antoni. 2018. The Learnability of Symbolic Automata. In International Conference on Computer Aided Verification (CAV). Springer, 427–445.
[10]
Gérard Basler, Michele Mazzucchi, Thomas Wahl, and Daniel Kroening. 2009. Symbolic counter abstraction for concurrent software. In International Conference on Computer Aided Verification (CAV). Springer, 64–78.
[11]
Jaroslav Bendík and Ivana Černá. 2020. MUST: minimal unsatisfiable subsets enumeration tool. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 135–152.
[12]
Jaroslav Bendík, Ivana Černá, and Nikola Beneš. 2018. Recursive online enumeration of all minimal unsatisfiable subsets. In Automated Technology for Verification and Analysis (ATVA). Springer, 143–159.
[13]
Michael Benedikt, Leonid Libkin, Thomas Schwentick, and Luc Segoufin. 2003. Definable Relations and First-Order Query Languages over Strings. Journal of the ACM (JACM), 50, 5 (2003), 694–751.
[14]
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder. 2015. Decidability of Parameterized Verification. Morgan & Claypool Publishers.
[15]
Achim Blumensath and Erich Gradel. 2000. Automatic Structures. In Symposium on Logic in Computer Science (LICS). IEEE, 51–62.
[16]
Achim Blumensath and Erich Grädel. 2004. Finite Presentations of Infinite Structures: Automata and Interpretations. Theory of Computing Systems (TCS), 37, 6 (2004), 641–674.
[17]
Ahmed Bouajjani, Peter Habermehl, and Tomáš Vojnar. 2004. Abstract Regular Model Checking. In International Conference on Computer-Aided Verification (CAV). Springer, 372–386.
[18]
Ahmed Bouajjani, Bengt Jonsson, Marcus Nilsson, and Tayssir Touili. 2000. Regular Model Checking. In International Conference on Computer-Aided Verification (CAV). Springer, 403–418.
[19]
Aaron R. Bradley and Zohar Manna. 1998. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer.
[20]
Aaron R. Bradley, Zohar Manna, and Henny B. Sipma. 2006. What’s Decidable about Arrays? In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer, 427–442.
[21]
Ernest Chang and Rosemary Roberts. 1979. An Improved Algorithm for Decentralized Extrema-Finding in Circular Configurations of Processes. Communications of the ACM (CACM), 22, 5 (1979), 281–283.
[22]
Yu-Fang Chen, Chih-Duo Hong, Anthony W. Lin, and Philipp Rümmer. 2017. Learning to Prove Safety over Parameterised Concurrent Systems. In International Conference on Formal Methods in Computer-Aided Design (FMCAD). Springer, 76–83.
[23]
Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. 2014. IC3 Modulo Theories via Implicit Predicate Abstraction. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 46–61.
[24]
Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. 2016. Infinite-state invariant checking with IC3 and predicate abstraction. Formal Methods in System Design, 49 (2016), 190–218.
[25]
Alessandro Cimatti, Alberto Griggio, and Gianluca Redondi. 2022. Verification of SMT Systems with Quantifiers. In International Symposium on Automated Technology for Verification and Analysis (ATVA). Springer, 154–170.
[26]
Alessandro Cimatti, Alberto Griggio, and Gianluca Redondi. 2021. Universal Invariant Checking of Parametric Systems with Quantifier-free SMT Reasoning. In International Conference on Automated Deduction (CADE). Springer, 131–147.
[27]
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–141.
[28]
Edmund Clarke, Murali Talupur, and Helmut Veith. 2008. Proving Ptolemy Right: The Environment Abstraction Framework for Model Checking Concurrent Systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 33–47.
[29]
Edmund M. Clarke, Orna Grumberg, and Michael C. Browne. 1986. Reasoning about Networks with Many Identical Finite State Processes. In Symposium on Principles of Distributed Computing (PODC). ACM, 240–248.
[30]
Edmund M. Clarke Jr, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. 2018. Model Checking. MIT press.
[31]
Thomas Colcombet and Christof Löding. 2007. Transforming Structures by Set Interpretations. Logical Methods in Computer Science (LMCS), 3, 2 (2007), paper–4.
[32]
Byron Cook, Andreas Podelski, and Andrey Rybalchenko. 2007. Proving Thread Termination. In Programming Language Design and Implementation (PLDI). ACM, 320–330.
[33]
Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Symposium on Principles of Programming Languages (POPL). ACM, 238–252.
[34]
Jakub Daniel, Alessandro Cimatti, Alberto Griggio, Stefano Tonetta, and Sergio Mover. 2016. Infinite-State Liveness-To-Safety via Implicit Abstraction and Well-Founded Relations. In International Conference on Computer-Aided Verification (CAV). Springer, 271–291.
[35]
Leonardo Mendonça de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 337–340.
[36]
Stéphane Demri, Valentin Goranko, and Martin Lange. 2016. Temporal logics in computer science: finite-state systems. 58, Cambridge University Press.
[37]
Edsger W. Dijkstra. 1982. Self-Stabilization in Spite of Distributed Control. In Selected Writings on Computing: A Personal Perspective. Springer, 41–46.
[38]
Alastair Donaldson, Alexander Kaiser, Daniel Kroening, and Thomas Wahl. 2011. Symmetry-aware predicate abstraction for shared-variable concurrent programs. In International Conference on Computer-Aided Verification (CAV). Springer, 356–371.
[39]
Alastair F. Donaldson, Alexander Kaiser, Daniel Kroening, Michael Tautschnig, and Thomas Wahl. 2012. Counterexample-Guided Abstraction Refinement for Symmetric Concurrent Programs. Formal Methods in System Design (FMSD), 41, 1 (2012), 25–44.
[40]
Samuel Drews and Loris D’Antoni. 2017. Learning Symbolic Automata. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 10205, Springer, 173–189.
[41]
E. Allen Emerson and Kedar S. Namjoshi. 2003. On Reasoning about Rings. International Journal of Foundations of Computer Science, 14, 04 (2003), 527–549.
[42]
Javier Esparza, Andreas Gaiser, and Stefan Kiefer. 2012. Proving termination of probabilistic programs using patterns. In International Conference on Computer-Aided Verification (CAV). Springer, 123–138.
[43]
Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. 2016. Proving Liveness of Parameterized Programs. In Symposium on Logic in Computer Science (LICS). IEEE, 1–12.
[44]
Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, and Aarti Gupta. 2019. Quantified Invariants via Syntax-Guided Synthesis. In Computer Aided Verification (CAV). Springer, 259–277.
[45]
Paolo Felli, Alessandro Gianola, and Marco Montali. 2021. SMT-based safety checking of parameterized multi-agent systems. In Proceedings of the AAAI Conference on Artificial Intelligence (AAAI). 35, PKP Publishing, 6321–6330.
[46]
Tomáš Fiedor, Lukáš Holík, Petr Janků, Ondřej Lengál, and Tomáš Vojnar. 2017. Lazy Automata Techniques for WS1S. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 407–425.
[47]
Cormac Flanagan and Shaz Qadeer. 2002. Predicate Abstraction for Software Verification. In Symposium on Principles of Programming Languages (POPL). ACM, 191–202.
[48]
Zeinab Ganjei, Ahmed Rezine, Petru Eles, and Zebo Peng. 2016. Counting dynamically synchronizing processes. International Journal on Software Tools for Technology Transfer (STTT), 18 (2016), 517–534.
[49]
Yeting Ge and Leonardo De Moura. 2009. Complete Instantiation for Quantified Formulas in Satisfiability Modulo Theories. In International Conference on Computer Aided Verification (CAV). Springer, 306–320.
[50]
Steven M. German and A. Prasad Sistla. 1992. Reasoning about Systems with Many Processes. Journal of the ACM (JACM), 39, 3 (1992), 675–735.
[51]
Silvio Ghilardi, Alessandro Gianola, and Deepak Kapur. 2021. Interpolation and Amalgamation for Arrays with MaxDiff. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS). Springer, 268–288.
[52]
Silvio Ghilardi, Enrica Nicolini, Silvio Ranise, and Daniele Zucchelli. 2008. Towards SMT Model Checking of Array-Based Systems. In International Joint Conference on Automated Reasoning (IJCAR). Springer, 67–82.
[53]
Silvio Ghilardi and Silvio Ranise. 2010. MCMT: A Model Checker Modulo Theories. In International Joint Conference on Automated Reasoning (IJCAR). Springer, 22–29.
[54]
Arie Gurfinkel, Sharon Shoham, and Yuri Meshman. 2016. SMT-Based Verification of Parameterized Systems. In International Symposium on Foundations of Software Engineering (FSE). ACM, 338–348.
[55]
Arie Gurfinkel, Sharon Shoham, and Yakir Vizel. 2018. Quantifiers on Demand. In Automated Technology for Verification and Analysis (ATVA). Springer, 248–266.
[56]
Peter Habermehl, Radu Iosif, and Tomáš Vojnar. 2008. A Logic of Singly Indexed Arrays. In International Conference on Logic Programming and Automated Reasoning (LPAR). Springer, 558–573.
[57]
Ian Hodkinson, Frank Wolter, and Michael Zakharyaschev. 2000. Decidable Fragments of First-Order Temporal Logics. In Annals of Pure and Applied Logic. Elsevier, 181–185.
[58]
Jochen Hoenicke and Tanja Schindler. 2018. Efficient interpolation for the theory of arrays. In International Joint Conference on Automated Reasoning (IJCAR). Springer, 549–565.
[59]
Chih-Duo Hong. 2022. Symbolic techniques for parameterised verification. Ph. D. Dissertation. University of Oxford.
[60]
Ranjit Jhala and Kenneth L. McMillan. 2007. Array Abstractions from Proofs. In International Conference on Computer-Aided Verification (CAV). Springer, 193–206.
[61]
Ranjit Jhala, Andreas Podelski, and Andrey Rybalchenko. 2018. Predicate Abstraction for Program Verification: Safety and Termination. In Handbook of Model Checking. Springer, 447–491.
[62]
Alexander Kaiser, Daniel Kroening, and Thomas Wahl. 2017. Lost in abstraction: Monotonicity in multi-threaded programs. Information and Computation, 252 (2017), 30–47.
[63]
Jeroen Ketema and Alastair F. Donaldson. 2017. Termination Analysis for GPU Kernels. Science of Computer Programming, 148 (2017), 107–122.
[64]
Nils Klarlund and Anders Møller. 2001. Mona Version 1.4: User Manual. BRICS, Department of Computer Science, University of Aarhus Denmark.
[65]
Nils Klarlund, Anders Møller, and Michael I. Schwartzbach. 2002. MONA Implementation Secrets. International Journal of Foundations of Computer Science, 13, 04 (2002), 571–586.
[66]
Anvesh Komuravelli, Nikolaj S. Bjørner, Arie Gurfinkel, and Kenneth L. McMillan. 2015. Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays. In Formal Methods in Computer-Aided Design (FMCAD). IEEE, 89–96.
[67]
Daniel Kroening and Ofer Strichman. 2016. Decision Procedures. Springer.
[68]
Shuvendu K. Lahiri and Randal E. Bryant. 2004. Constructing Quantified Invariants via Predicate Abstraction. In International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Springer, 267–281.
[69]
Shuvendu K. Lahiri and Randal E. Bryant. 2004. Indexed Predicate Discovery for Unbounded System Verification. In International Conference on Computer-Aided Verification (CAV). Springer, 135–147.
[70]
Shuvendu K. Lahiri and Randal E. Bryant. 2007. Predicate Abstraction with Indexed Predicates. ACM Transactions on Computational Logic (TOCL), 9, 1 (2007), 4–es.
[71]
Mark H. Liffiton, Alessandro Previti, Ammar Malik, and Joao Marques-Silva. 2016. Fast, flexible MUS enumeration. Constraints, 21 (2016), 223–250.
[72]
Anthony W. Lin and Philipp Rümmer. 2016. Liveness of Randomised Parameterised Systems under Arbitrary Schedulers. In International Conference on Computer-Aided Verification (CAV). Springer, 112–133.
[73]
Anthony W. Lin and Philipp Rümmer. 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–114.
[74]
Haojun Ma, Aman Goel, Jean-Baptiste Jeannin, Manos Kapritsos, Baris Kasikci, and Karem A Sakallah. 2019. I4: incremental inference of inductive invariants for verification of distributed protocols. In The Symposium on Operating Systems Principles (SOSP). ACM, 370–384.
[75]
Alexander Malkis, Andreas Podelski, and Andrey Rybalchenko. 2007. Precise thread-modular verification. In International Static Analysis Symposium (SAS). Springer, 218–232.
[76]
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–147.
[77]
Zohar Manna and Amir Pnueli. 2012. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer Science & Business Media.
[78]
John McCarthy. 1993. Towards a mathematical science of computation. Program Verification: Fundamental Issues in Computer Science, 1, 1 (1993), 35–56.
[79]
Kenneth L. McMillan. 2008. Quantified Invariant Generation Using an Interpolating Saturation Prover. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 413–427.
[80]
Kenneth L. McMillan. 2018. Eager Abstraction for Symbolic Model Checking. In International Conference on Computer Aided Verification (CAV). Springer, 191–208.
[81]
Kenneth L. McMillan and Oded Padon. 2018. Deductive Verification in Decidable Fragments with Ivy. In International Static Analysis Symposium (SAS). Springer, 43–55.
[82]
Kenneth L. McMillan and Oded Padon. 2020. Ivy: A Multi-Modal Verification Tool for Distributed Algorithms. In International Conference on Computer Aided Verification (CAV). Springer, 190–202.
[83]
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–33.
[84]
Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, and Sharon Shoham. 2021. Temporal prophecy for proving temporal properties of infinite-state systems. Formal Methods in System Design (FMSD), 57 (2021), 246–269.
[85]
Thomas Pani, Georg Weissenbacher, and Florian Zuleger. 2021. Rely-guarantee bound analysis of parameterized concurrent shared-memory programs: With an application to proving that non-blocking algorithms are bounded lock-free. Formal Methods in System Design (FMSD), 57, 2 (2021), 270–302.
[86]
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–38.
[87]
Matan I Peled, Bat-Chen Rothenberg, and Shachar Itzhaky. 2023. SMT sampling via model-guided approximation. In International Symposium on Formal Methods (FM). Springer, 74–91.
[88]
Corneliu Popeea and Andrey Rybalchenko. 2012. Compositional Termination Proofs for Multi-Threaded Programs. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Springer, 237–251.
[89]
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–44.
[90]
Viktor Schuppan and Armin Biere. 2006. Liveness Checking as Safety Checking for Infinite State Spaces. Electronic Notes in Theoretical Computer Science (ENTCS), 149, 1 (2006), 79–96.
[91]
Mohamed Nassim Seghir, Andreas Podelski, and Thomas Wies. 2009. Abstraction Refinement for Quantified Array Assertions. In Static Analysis Symposium (SAS). Springer, 3–18.
[92]
Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang, and Bo-Yin Yang. 2021. CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver. In International Conference on Computer Aided Verification (CAV). Springer, 149–171.
[93]
Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv, Sharon Shoham, James R. Wilcox, and Doug Woos. 2018. Modularity for Decidability of Deductive Verification with Applications to Distributed Systems. In Conference on Programming Language Design and Implementation (PLDI). ACM, 662–677.
[94]
Dirk van Dalen. 1994. Logic and structure. 3, Springer.
[95]
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–331.
[96]
Peisen Yao, Qingkai Shi, Heqing Huang, and Charles Zhang. 2020. Fast bit-vector satisfiability. In International Symposium on Software Testing and Analysis (ISSTA). ACM, 38–50.
Index Terms
- Regular Abstractions for Array Systems
Recommendations
Regular model checking for LTL(MSO)
Regular model checking is a form of symbolic model checking for parameterized and infinite-state systems whose states can be represented as words of arbitrary length over a finite alphabet, in which regular sets of words are used to represent sets of ...
Abstract regular (tree) model checking
Regular model checking is a generic technique for verification of infinite-state and/or parametrised systems which uses finite word automata or finite tree automata to finitely represent potentially infinite sets of reachable configurations of the ...
Abstract Regular Tree Model Checking
Regular (tree) model checking (RMC) is a promising generic method for formal verification of infinite-state systems. It encodes configurations of systems as words or trees over a suitable alphabet, possibly infinite sets of configurations as finite word ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2024
2820 pages
Copyright © 2024 Owner/Author.
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 05 January 2024
Published in PACMPL Volume 8, Issue POPL
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 279Total Downloads
- Downloads (Last 12 months)279
- Downloads (Last 6 weeks)31
Reflects downloads up to 12 Dec 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in