Array Folds Logic

DOI10.1007/978-3-319-41540-6_13MaRDI QIDQ4633555zbMATH OpenOpenAlexFDO

Authors Przemysław Daca, Andrey Kupriyanov, Thomas A. Henzinger

Publication date 3 May 2019

Published in Computer Aided Verification (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1603.06850

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70)

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 occurs frequently in real-life programs. We provide a tool that can discharge proof obligations in AFL, and we demonstrate on practical examples that our decision procedure can solve a broad range of problems in symbolic testing and program verification.

Recommendations

• Graph folding and programmable logic array
• scientific article; zbMATH DE number 512955
• The Complexity of Near-Optimal Programmable Logic Array Folding
• Compatibility relation algorithm for the folding of programmable logic arrays
• A Logic of Singly Indexed Arrays
• scientific article; zbMATH DE number 2086236
• Packing arrays
• scientific article; zbMATH DE number 1284435

Cited in

(10)

• Succinct ordering and aggregation constraints in algebraic array theories
• A solver for arrays with concatenation
• A program instrumentation framework for automatic verification
• Generalized arrays for Stainless frames
• On algebraic array theories
• What's decidable about arrays with sums?
• NP satisfiability for arrays as powers
• Reasoning on data words over numeric domains
• Interpolating parametric array theories
• Automatic program instrumentation for automatic verification

This page was built for publication: Array Folds Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4633555)