Removing algebraic data types from constrained Horn clauses using difference predicates (Q2096439): Difference between revisions

@@ Property / describes a project that uses @@
+Spacer
@@ Property / describes a project that uses: Spacer / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Zeno
@@ Property / describes a project that uses: Zeno / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HipSpec
@@ Property / describes a project that uses: HipSpec / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+VeriMAP
@@ Property / describes a project that uses: VeriMAP / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CVC4
@@ Property / describes a project that uses: CVC4 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+IsaPlanner
@@ Property / describes a project that uses: IsaPlanner / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+PVS
@@ Property / describes a project that uses: PVS / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+OCaml
@@ Property / describes a project that uses: OCaml / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+MathSAT5
@@ Property / describes a project that uses: MathSAT5 / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / OpenAlex ID @@
+W3100001578
@@ Property / OpenAlex ID: W3100001578 / rank @@
+Normal rank
@@ Property / cites work @@
+Computer aided verification. 23rd international conference, CAV 2011, Snowbird, UT, USA, July 14--20, 2011. Proceedings
+Normal rank
@@ Property / cites work @@
+Satisfiability Modulo Theories
@@ Property / cites work: Satisfiability Modulo Theories / 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 @@
+Q2751365
@@ Property / cites work: Q2751365 / rank @@
+Normal rank
@@ Property / cites work @@
+The MathSAT5 SMT Solver
@@ Property / cites work: The MathSAT5 SMT Solver / rank @@
+Normal rank
@@ Property / cites work @@
+Automating Inductive Proofs Using Theory Exploration
+Normal rank
@@ Property / cites work @@
+Relational verification through Horn clause transformation
+Normal rank
@@ Property / cites work @@
+Solving Horn Clauses on Inductive Data Types Without Induction
+Normal rank
@@ Property / cites work @@
+Q5016384
@@ Property / cites work: Q5016384 / rank @@
+Normal rank
@@ Property / cites work @@
+Q4052071
@@ Property / cites work: Q4052071 / rank @@
+Normal rank
@@ Property / cites work @@
+Transformations of CLP modules
@@ Property / cites work: Transformations of CLP modules / rank @@
+Normal rank
@@ Property / cites work @@
+Program Development in Computational Logic
@@ Property / cites work: Program Development in Computational Logic / rank @@
+Normal rank
@@ Property / cites work @@
+Generalization strategies for the verification of infinite state systems
+Normal rank
@@ Property / cites work @@
+Generalized Property Directed Reachability
@@ Property / cites work: Generalized Property Directed Reachability / rank @@
+Normal rank
@@ Property / cites work @@
+Productive use of failure in inductive proof
@@ Property / cites work: Productive use of failure in inductive proof / rank @@
+Normal rank
@@ Property / cites work @@
+Case-Analysis for Rippling and Inductive Proof
@@ Property / cites work: Case-Analysis for Rippling and Inductive Proof / rank @@
+Normal rank
@@ Property / cites work @@
+Automating Induction with an SMT Solver
@@ Property / cites work: Automating Induction with an SMT Solver / rank @@
+Normal rank
@@ Property / cites work @@
+Q3992908
@@ Property / cites work: Q3992908 / rank @@
+Normal rank
@@ Property / cites work @@
+Isabelle/HOL. A proof assistant for higher-order logic
+Normal rank
@@ Property / cites work @@
+Reasoning about algebraic data types with abstractions
+Normal rank
@@ Property / cites work @@
+Induction for SMT Solvers
@@ Property / cites work: Induction for SMT Solvers / rank @@
+Normal rank
@@ Property / cites work @@
+On Inductive and Coinductive Proofs via Unfold/Fold Transformations
+Normal rank
@@ Property / cites work @@
+Zeno: An Automated Prover for Properties of Recursive Data Structures
+Normal rank
@@ Property / cites work @@
+Automating induction for solving Horn clauses
@@ Property / cites work: Automating induction for solving Horn clauses / rank @@
+Normal rank