A Solver for Arrays with Concatenation

Qinshi Wang, Andrew W. Appel

Research output: Contribution to journalArticlepeer-review

2 Scopus citations

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.

Original languageEnglish (US)
Article number4
JournalJournal of Automated Reasoning
Volume67
Issue number1
DOIs
StatePublished - Mar 2023

All Science Journal Classification (ASJC) codes

  • Software
  • Computational Theory and Mathematics
  • Artificial Intelligence

Keywords

  • Array theory
  • Correctness proof
  • Decision procedure
  • Program verification
  • Proof automation

Fingerprint

Dive into the research topics of 'A Solver for Arrays with Concatenation'. Together they form a unique fingerprint.

Cite this