Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

A Solver for Arrays with Concatenation

A Solver for Arrays with Concatenation The theory of arrays has been widely investigated. But concatenation, an operator that consistently appears in specifications of functional-correctness verification tools (e.g., Dafny, VeriFast, VST), is not included in most variants of the theory. Arrays with concatenation need better solvers with theoretical guarantees. We formalize a theory of arrays with concatenation, and define the array property fragment with concatenation. Although the array property fragment without concatenation is decidable, the fragment with concatenation is undecidable in general (e.g., when the base theory for array elements is linear integer arithmetic). But we characterize a “tangle-free” fragment; we present an algorithm that classifies verification goals in the array property fragment with concatenation as tangle-free or entangled, and that decides validity of tangle-free goals. We implement the algorithm in Coq and apply it to functional-correctness verification of C programs. The result shows our algorithm is reasonably efficient and reduces a significant amount of human effort in verification tasks. We also give an algorithm for using this array theory solver as a theory solver in SMT solvers. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Journal of Automated Reasoning Springer Journals

A Solver for Arrays with Concatenation

Loading next page...
 
/lp/springer-journals/a-solver-for-arrays-with-concatenation-aDcXrtMSsm
Publisher
Springer Journals
Copyright
Copyright © The Author(s), under exclusive licence to Springer Nature B.V. 2023. Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
ISSN
0168-7433
eISSN
1573-0670
DOI
10.1007/s10817-022-09654-y
Publisher site
See Article on Publisher Site

Abstract

The theory of arrays has been widely investigated. But concatenation, an operator that consistently appears in specifications of functional-correctness verification tools (e.g., Dafny, VeriFast, VST), is not included in most variants of the theory. Arrays with concatenation need better solvers with theoretical guarantees. We formalize a theory of arrays with concatenation, and define the array property fragment with concatenation. Although the array property fragment without concatenation is decidable, the fragment with concatenation is undecidable in general (e.g., when the base theory for array elements is linear integer arithmetic). But we characterize a “tangle-free” fragment; we present an algorithm that classifies verification goals in the array property fragment with concatenation as tangle-free or entangled, and that decides validity of tangle-free goals. We implement the algorithm in Coq and apply it to functional-correctness verification of C programs. The result shows our algorithm is reasonably efficient and reduces a significant amount of human effort in verification tasks. We also give an algorithm for using this array theory solver as a theory solver in SMT solvers.

Journal

Journal of Automated ReasoningSpringer Journals

Published: Mar 1, 2023

Keywords: Array theory; Program verification; Decision procedure; Correctness proof; Proof automation

References