Array theory of bounded elements and its applications (Q2351149): Difference between revisions

@@ Property / describes a project that uses @@
+Boolector
@@ Property / describes a project that uses: Boolector / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+STP
@@ Property / describes a project that uses: STP / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/s10817-013-9293-6
+Normal rank
@@ Property / OpenAlex ID @@
+W2029989893
@@ Property / OpenAlex ID: W2029989893 / rank @@
+Normal rank
@@ Property / cites work @@
+Automatic Verification of Integer Array Programs
@@ Property / cites work: Automatic Verification of Integer Array Programs / rank @@
+Normal rank
@@ Property / cites work @@
+Verification, Model Checking, and Abstract Interpretation
+Normal rank
@@ Property / cites work @@
+Q3181652
@@ Property / cites work: Q3181652 / rank @@
+Normal rank
@@ Property / cites work @@
+Weak Second‐Order Arithmetic and Finite Automata
+Normal rank
@@ Property / cites work @@
+Presburger arithmetic with unary predicates is <i>Π</i><sub>1</sub><sup>1</sup> complete
+Normal rank
@@ Property / cites work @@
+What’s Decidable about Sequences?
@@ Property / cites work: What’s Decidable about Sequences? / rank @@
+Normal rank
@@ Property / cites work @@
+A Decision Procedure for Bit-Vectors and Arrays
@@ Property / cites work: A Decision Procedure for Bit-Vectors and Arrays / rank @@
+Normal rank
@@ Property / cites work @@
+Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
+Normal rank
@@ Property / cites work @@
+Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
+Normal rank
@@ Property / cites work @@
+Decision procedures for extensions of the theory of arrays
+Normal rank
@@ Property / cites work @@
+Verification Decidability of Presburger Array Programs
+Normal rank
@@ Property / cites work @@
+A Logic of Singly Indexed Arrays
@@ Property / cites work: A Logic of Singly Indexed Arrays / rank @@
+Normal rank
@@ Property / cites work @@
+An axiomatic basis for computer programming
@@ Property / cites work: An axiomatic basis for computer programming / rank @@
+Normal rank
@@ Property / cites work @@
+Q4218939
@@ Property / cites work: Q4218939 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5613949
@@ Property / cites work: Q5613949 / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient E-Matching for SMT Solvers
@@ Property / cites work: Efficient E-Matching for SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+Efficiently solving quantified bit-vector formulas
+Normal rank