Counterexample-Guided Prophecy for Model Checking Modulo the Theory of Arrays (Q5043584): Difference between revisions

@@ Property / cites work @@
+Lazy Abstraction with Interpolants for Arrays
@@ Property / cites work: Lazy Abstraction with Interpolants for Arrays / rank @@
+Normal rank
@@ Property / cites work @@
+Booster: An Acceleration-Based Verification Framework for Array Programs
+Normal rank
@@ Property / cites work @@
+Q3181652
@@ Property / cites work: Q3181652 / rank @@
+Normal rank
@@ Property / cites work @@
+Horn Clause Solvers for Program Verification
@@ Property / cites work: Horn Clause Solvers for Program Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Quantifier-Free Interpolation of a Theory of Arrays
+Normal rank
@@ Property / cites work @@
+Q5310200
@@ Property / cites work: Q5310200 / rank @@
+Normal rank
@@ Property / cites work @@
+Verification, Model Checking, and Abstract Interpretation
+Normal rank
@@ Property / cites work @@
+SAT-Based Model Checking without Unrolling
@@ Property / cites work: SAT-Based Model Checking without Unrolling / rank @@
+Normal rank
@@ Property / cites work @@
+Satisfiability Modulo Theories
@@ Property / cites work: Satisfiability Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Incremental Linearization for Satisfiability and Verification Modulo Nonlinear Arithmetic and Transcendental Functions
+Normal rank
@@ Property / cites work @@
+Infinite-state invariant checking with IC3 and predicate abstraction
+Normal rank
@@ Property / cites work @@
+Universal invariant checking of parametric systems with quantifier-free SMT reasoning
+Normal rank
@@ Property / cites work @@
+Computing Small Unsatisfiable Cores in Satisfiability Modulo Theories
+Normal rank
@@ Property / cites work @@
+The MathSAT5 SMT Solver
@@ Property / cites work: The MathSAT5 SMT Solver / rank @@
+Normal rank
@@ Property / cites work @@
+Weakly Equivalent Arrays
@@ Property / cites work: Weakly Equivalent Arrays / rank @@
+Normal rank
@@ Property / cites work @@
+Counterexample-guided abstraction refinement for symbolic model checking
+Normal rank
@@ Property / cites work @@
+Local proofs for global safety properties
@@ Property / cites work: Local proofs for global safety properties / rank @@
+Normal rank
@@ Property / cites work @@
+Linear reasoning. A new form of the Herbrand-Gentzen theorem
+Normal rank
@@ Property / cites work @@
+MCMT: A Model Checker Modulo Theories
@@ Property / cites work: MCMT: A Model Checker Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Quantifiers on demand
@@ Property / cites work: Quantifiers on demand / rank @@
+Normal rank
@@ Property / cites work @@
+Q4003410
@@ Property / cites work: Q4003410 / rank @@
+Normal rank
@@ Property / cites work @@
+Global guidance for local generalization in model checking
+Normal rank
@@ Property / cites work @@
+SMT-based model checking for recursive programs
@@ Property / cites work: SMT-based model checking for recursive programs / rank @@
+Normal rank
@@ Property / cites work @@
+Quantified Heap Invariants for Object-Oriented Programs
+Normal rank
@@ Property / cites work @@
+Decision procedures. An algorithmic point of view
@@ Property / cites work: Decision procedures. An algorithmic point of view / rank @@
+Normal rank
@@ Property / cites work @@
+Computer Aided Verification
@@ Property / cites work: Computer Aided Verification / rank @@
+Normal rank
@@ Property / cites work @@
+Quantified Invariant Generation Using an Interpolating Saturation Prover
+Normal rank
@@ Property / cites work @@
+Eager abstraction for symbolic model checking
@@ Property / cites work: Eager abstraction for symbolic model checking / rank @@
+Normal rank
@@ Property / cites work @@
+Cell morphing: from array programs to array-free Horn clauses
+Normal rank
@@ Property / cites work @@
+Counterexample-guided prophecy for model checking modulo the theory of arrays
+Normal rank
@@ Property / cites work @@
+An axiomatic proof technique for parallel programs
+Normal rank
@@ Property / cites work @@
+Temporal prophecy for proving temporal properties of infinite-state systems
+Normal rank
@@ Property / cites work @@
+Q5020662
@@ Property / cites work: Q5020662 / rank @@
+Normal rank