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.
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Notes
Concatenation is a computable function and is easy to use in a functional program that defines the behavior of the original program. Without using concatentation, it is not simple to compute the value of an array characterized by quantified formulas.
Not only in our own program verifications: We examined the VigNAT [24] proofs (github.com/vignat) in files
and
. Of the 73 lemmas in
, 50 are expressible in our theory. The rest of lemmas involve operators unsupported in our theory, e.g. filter and elements-are-distinct. Of these, 37 lemmas are quantifier-free (hence tangle-free) and 13 lemmas are quantified and tangle-free; none are entangled. (We determined this by inspection—none have the kind of recurrence that would lead to entanglement.) All 50 lemmas would be solved by our solver. In fact, if VeriFast had been equipped with our solver, none of these 50 lemmas in
would be needed. The file
has 110 lines of C code and 2500 lines of specification and proof. Within the proof there are approximately 100 applications of list-operation lemmas (such as the ones in
,
, and
) which could be fully or partially automated using our solver—which would significantly reduce the number of lines of human-written proof-script. In all of these subgoals we did not identify any that have the kind of recurrence that would lead to entanglement.
One can also perform a more precise (but more expensive) analysis by checking the validity of \(\varDelta '\), defined as \(\lnot \psi _2 \implies \bigwedge _{(u, v, w)\in E\setminus F} \delta (u)+w=\delta (v),\) where \(\psi _2\) is the instantiation of \(\psi _1\) constructed in Sect. 3.5. This classifies more goals as tangle-free. The validity of \(\varDelta '\) depends on the choice of F and reference nodes.
To give more hints, the algorithm may also identify the off-forest edge which causes the unprovable equation, then reconstruct and print the nonzero cycle—see §8.
Replacing arbitrary quantifiers over Z in negative positions with finitely many instantiations is sound (if the resulting formula is valid, then the original formula is also valid), but not complete (the opposite direction as soundness). [4]
or \(\varDelta '\) is valid; see footnote 3.
As discussed in §7, we believe our algorithm is fast but our implementation is slow because of the use of Ltac.
Two-case \(i=j,~i\not =j\) case splits, rather than three-case \(i<j,~i=j,~i>j\).
We can decide it because the correctness results in Sect. 4 can be generalized to the case that the IPG has more edges than the queried formula \(\varphi _i\wedge ar'(R)\).
In the array solver, \(a\ne b\) is treated as a shorthand for \(\left| a\right| \ne \left| b\right| \ \vee \ \exists i.\ 0\le i<\left| a\right| \wedge {a}[i]\ne {b}[i]\). The existentially quantified i can be treated as a free variable, so it is quantifier-free.
References
Abdulla, P.A., Atig, M.F., Chen, Y.-F., Holík, L., Rezine, A., Rümmer, P., Stenman, J.: String constraints for verification. In: International Conference on Computer Aided Verification, pp. 150–166. Springer (2014). https://doi.org/10.1007/978-3-319-08867-9_10
Abdulla, P.A., Atig, M.F., Diep, B.P., Holík, L., Janků, P.: Chain-free string constraints. In: International Symposium on Automated Technology for Verification and Analysis, pp. 277–293. Springer (2019). https://doi.org/10.1007/978-3-030-31784-3_16
Appel, A.W.: Verified software toolchain. In: European Symposium on Programming, pp. 1–17. Springer (2011). https://doi.org/10.1007/978-3-642-19718-5_1
Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp. 305–343. Springer (2018). https://doi.org/10.1007/978-3-319-10575-8_11
Besson, F., Cornilleau, P.-E., Pichardie, D.: Modular SMT proofs for fast reflexive checking inside coq. In: International Conference on Certified Programs and Proofs, pp. 151–166. Springer (2011). https://doi.org/10.1007/978-3-642-25379-9_13
Bjørner, N., Ganesh, V., Michel, R., Veanes, M.: An SMT-LIB format for sequences and regular expressions. SMT 12, 76–86 (2012)
Bradley, A.R., Manna, Z., Sipma,H.B.: What’s decidable about arrays? In: International Workshop on Verification, Model Checking, and Abstract Interpretation, pp. 427–442. Springer (2006). https://doi.org/10.1007/11609773_28
Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-Floyd: a separation logic tool to verify correctness of C programs. J. Autom. Reason. 61(1–4), 367–422 (2018). https://doi.org/10.1007/s10817-018-9457-5
Chen, T., Chen, Y., Hague, M., Lin, A.W., Wu, Z..: What is decidable about string constraints with the replaceall function. In: Proceedings of the ACM on Programming Languages, 2(POPL):1–29 (2017). https://doi.org/10.1145/3158091
Daca, P., Henzinger, T.A., Kupriyanov, A.: Array folds logic. In: International Conference on Computer Aided Verification, pp. 230–248. Springer (2016). https://doi.org/10.1007/978-3-319-41540-6_13
Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what’s decidable? In: Haifa Verification Conference, pp. 209–226. Springer (2012). https://doi.org/10.1007/978-3-642-39611-3_21
Ge, Y., De Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: International Conference on Computer Aided Verification, pp. 306–320. Springer (2009). https://doi.org/10.1007/978-3-642-02658-4_25
Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: International Conference on Foundations of Software Science and Computational Structures, pp. 474–489. Springer (2008). https://doi.org/10.1007/978-3-540-78499-9_33
Holík, L., Janků, P., Lin, A.W., Rümmer, P., Vojnar, T.: String constraints with concatenation and transducers solved efficiently. In: Proceedings of the ACM on Programming Languages 2(POPL), pp. 1–32 (2017). https://doi.org/10.1145/3158092
Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: Verifast: A powerful, sound, predictable, fast verifier for C and Java. In: NASA Formal Methods Symposium, pp. 41–55. Springer (2011). https://doi.org/10.1007/978-3-642-20398-5_4
Leino, K., Rustan, M.: Dafny: An automatic program verifier for functional correctness. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp. 348–370. Springer (2010). https://doi.org/10.1007/978-3-642-17511-4_20
Lin, A.W., Barceló, P.: String solving with word equations and transducers: towards a logic for analysing mutation XSS. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 123–136 (2016). https://doi.org/10.1145/2837614.2837641
Makanin, G.S.: The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik 145(2), 147–236 (1977)
McCarthy, J.: Towards a mathematical science of computation. In: Program Verification, pp. 35–56. Springer (1993). https://doi.org/10.1007/978-94-011-1793-7_2
Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc, Hoboken (1967)
Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. J. ACM 51(3), 483–496 (2004). https://doi.org/10.1145/990308.990312
Plandowski, W.: An efficient algorithm for solving word equations. In: Proceedings of the Thirty-Eighth Annual ACM Symposium on Theory of Computing, pp. 467–476. ACM (2006). https://doi.org/10.1145/1132516.1132584
Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp. 29–37. IEEE (2001)
Zaostrovnykh, A., Pirelli, S., Pedrosa, L., Argyraki, K., Candea, G.: A formally verified NAT. In: Proceedings of the Conference of the ACM Special Interest Group on Data Communication (SIGCOMM’17), pp. 141–154 (2017)
Zheng, Y., Ganesh, V., Subramanian, S., Tripp, O., Berzish, M., Dolby, J., Zhang, X.: Z3str2: an efficient solver for strings, regular expressions, and length constraints. Formal Methods System Des 50(2–3), 249–288 (2017). https://doi.org/10.1007/s10703-016-0263-6
Funding
This work was funded in part by the National Science Foundation under grant CCF-1521602 and DARPA under contract HR001120C0160.
Author information
Authors and Affiliations
Corresponding author
Ethics declarations
Conflicts of interest
There are no conflicts of interest. Code is available open-source as described in the paper.
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
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.
About this article
Cite this article
Wang, Q., Appel, A.W. A Solver for Arrays with Concatenation. J Autom Reasoning 67, 4 (2023). https://doi.org/10.1007/s10817-022-09654-y
Received:
Accepted:
Published:
DOI: https://doi.org/10.1007/s10817-022-09654-y