Array Folds Logic
Przemys{\l}aw Daca, Thomas A. Henzinger, Andrey Kupriyanov

TL;DR
Array Folds Logic (AFL) extends array theories to include counting properties, enabling concise expression of array characteristics and supporting practical verification tasks with a decision procedure.
Contribution
Introduces AFL, a new array logic with counting capabilities, and demonstrates its decidability, practical utility, and limitations in expressiveness and complexity.
Findings
AFL is PSPACE-complete for satisfiability.
Adding quantifiers or concatenation leads to undecidability.
The tool can solve diverse verification problems.
Abstract
We present an extension to the quantifier-free theory of integer arrays which allows us to express counting. The properties expressible in Array Folds Logic (AFL) include statements such as "the first array cell contains the array length," and "the array contains equally many minimal and maximal elements." These properties cannot be expressed in quantified fragments of the theory of arrays, nor in the theory of concatenation. Using reduction to counter machines, we show that the satisfiability problem of AFL is PSPACE-complete, and with a natural restriction the complexity decreases to NP. We also show that adding either universal quantifiers or concatenation leads to undecidability. AFL contains terms that fold a function over an array. We demonstrate that folding, a well-known concept from functional languages, allows us to concisely summarize loops that count over arrays, which…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Software Testing and Debugging Techniques · Logic, programming, and type systems
