Array theory of bounded elements and its applications
From MaRDI portal
Publication:2351149
DOI10.1007/s10817-013-9293-6zbMath1314.03017MaRDI 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
68Q60: Specification and verification (program logics, model checking, etc.)
03B25: Decidability of theories and sets of sentences
Related Items
Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure, Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure, Nested antichains for WS1S, Lazy Automata Techniques for WS1S
Uses Software
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 Π11 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
