Weakly equivalent arrays

DOI10.1007/978-3-319-24246-0_8MaRDI QIDQ2964457zbMATH OpenOpenAlexFDO

Authors Jürgen Christ, Jochen Hoenicke

Publication date 27 February 2017

Published in Frontiers of Combining Systems (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Data structures (68P05) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25)

Abstract: The (extensional) theory of arrays is widely used to model systems. Hence, efficient decision procedures are needed to model check such systems. Current decision procedures for the theory of arrays saturate the read-over-write and extensionality axioms originally proposed by McCarthy. Various filters are used to limit the number of axiom instantiations while preserving completeness. We present an algorithm that lazily instantiates lemmas based on weak equivalence classes. These lemmas are easier to interpolate as they only contain existing terms. We formally define weak equivalence and show correctness of the resulting decision procedure.

Recommendations

• Solving and interpolating constant arrays based on weak equivalences
• Decision procedures for extensions of the theory of arrays
• Array theory of bounded elements and its applications
• Verification, Model Checking, and Abstract Interpretation
• Decision procedures for flat array properties

Cites work

• scientific article; zbMATH DE number 5613976 (Why is no real title available?)
• Computer Aided Verification
• Frontiers of Combining Systems
• New results on rewrite-based satisfiability procedures
• Proof tree preserving interpolation
• Quantifier-free interpolation of a theory of arrays
• Term Rewriting and Applications
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory

Cited in

(11)

• Reasoning about vectors using an SMT theory of sequences
• Reasoning in the theory of heap: satisfiability and interpolation
• The map equality domain
• Counterexample-guided prophecy for model checking modulo the theory of arrays
• Combining combination properties: minimal models
• Reasoning about vectors: satisfiability modulo a theory of sequences
• What's decidable about arrays with sums?
• Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays
• Solving and interpolating constant arrays based on weak equivalences
• A Theory of Cartesian Arrays (with Applications in Quantum Circuit Verification)
• Reasoning over n-indexed sequences in SMT

Describes a project that uses

Uses Software

• SMTInterpol

This page was built for publication: Weakly equivalent arrays

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