Array theory of bounded elements and its applications

DOI10.1007/s10817-013-9293-6zbMath1314.03017OpenAlexW2029989893MaRDI QIDQ2351149

Ming Gu, Bow-Yaw Wang, Min Zhou, Fei He, Jia-Guang Sun

Publication date: 23 June 2015

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10817-013-9293-6

zbMATH Keywords

program verificationsatisfiability modulo theoriesarray theory

Mathematics Subject Classification ID

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

Related Items

Nested antichains for WS1S, Lazy Automata Techniques for WS1S, Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure, Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure

Uses Software

• Boolector
• z3
• MONA
• STP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Efficiently solving quantified bit-vector formulas
• Decision procedures for extensions of the theory of arrays
• Weak Second‐Order Arithmetic and Finite Automata
• Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
• Efficient E-Matching for SMT Solvers
• Automatic Verification of Integer Array Programs
• Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
• Verification Decidability of Presburger Array Programs
• Presburger arithmetic with unary predicates is Π₁¹ complete
• What’s Decidable about Sequences?
• A Decision Procedure for Bit-Vectors and Arrays
• A Logic of Singly Indexed Arrays
• An axiomatic basis for computer programming
• Verification, Model Checking, and Abstract Interpretation