Automating Induction with an SMT Solver (Q2891425): Difference between revisions

@@ Property / cites work @@
+Refinement Calculus
@@ Property / cites work: Refinement Calculus / rank @@
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
+Normal rank
@@ Property / cites work @@
+Sledgehammer: Judgement Day
@@ Property / cites work: Sledgehammer: Judgement Day / rank @@
+Normal rank
@@ Property / cites work @@
+Rippling: Meta-Level Guidance for Mathematical Reasoning
+Normal rank
@@ Property / cites work @@
+The ACL2 Sedan Theorem Proving System
@@ Property / cites work: The ACL2 Sedan Theorem Proving System / rank @@
+Normal rank
@@ Property / cites work @@
+Simplify: a theorem prover for program checking
@@ Property / cites work: Simplify: a theorem prover for program checking / 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 @@
+Q5585021
@@ Property / cites work: Q5585021 / rank @@
+Normal rank
@@ Property / cites work @@
+Dafny: An Automatic Program Verifier for Functional Correctness
+Normal rank
@@ Property / cites work @@
+A Polymorphic Intermediate Verification Language: Design and Logical Encoding
+Normal rank
@@ Property / cites work @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / rank @@
+Normal rank
@@ Property / cites work @@
+Zeno: An Automated Prover for Properties of Recursive Data Structures
+Normal rank