A Solver for Arrays with Concatenation

The theory of arrays has been widely investigated. But concatenation, an oper-ator that consistently appears in specifications o f f unctional-correctness v erification tools (e.g., Dafny, VeriFast, VST), is not included in most variants of the theory. Arrays with con-catenation need better solvers with theoretical guarantees. We formalize a theory of arrays with concatenation, and define t he a rray p roperty f ragment w ith c oncatenation. Although the array property fragment without concatenation is decidable, the fragment with concate-nation 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.