Weakly Equivalent Arrays

DOI10.1007/978-3-319-24246-0_8zbMath1471.68136arXiv1405.6939OpenAlexW2106750307MaRDI QIDQ2964457

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

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

Related Items (6)

Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays ⋮ The map equality domain ⋮ Reasoning about vectors: satisfiability modulo a theory of sequences ⋮ Counterexample-guided prophecy for model checking modulo the theory of arrays ⋮ Reasoning about vectors using an SMT theory of sequences ⋮ Reasoning in the theory of heap: satisfiability and interpolation

Uses Software

• SMTInterpol

Cites Work

• Unnamed Item
• Quantifier-Free Interpolation of a Theory of Arrays
• Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory
• New results on rewrite-based satisfiability procedures
• Computer Aided Verification
• Proof Tree Preserving Interpolation
• Frontiers of Combining Systems
• Term Rewriting and Applications

This page was built for publication: Weakly Equivalent Arrays