Automating Induction with an SMT Solver
From MaRDI portal
Recommendations
Cites work
- scientific article; zbMATH DE number 3303655 (Why is no real title available?)
- A polymorphic intermediate verification language: design and logical encoding
- Case-analysis for rippling and inductive proof
- Dafny: an automatic program verifier for functional correctness
- Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
- Refinement Calculus
- Rippling: Meta-Level Guidance for Mathematical Reasoning
- Simplify: a theorem prover for program checking
- Sledgehammer: judgement day
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- The ACL2 Sedan theorem proving system
- Zeno: an automated prover for properties of recursive data structures
Cited in
(17)- An assertional proof of the stability and correctness of Natural Mergesort
- Verifying Whiley programs with Boogie
- Triggerless happy. Intermediate verification with a first-order prover
- Automating theorem proving with SMT
- Adding decision procedures to SMT solvers using axioms with triggers
- Automating Inductive Proofs Using Theory Exploration
- TIP: tons of inductive problems
- Automata-driven automated induction
- Dafny
- Inductive benchmarks for automated reasoning
- Induction in saturation-based proof search
- Definitional Quantifiers Realise Semantic Reasoning for Proof by Induction
- Itauto: An Extensible Intuitionistic SAT Solver
- Tools and Algorithms for the Construction and Analysis of Systems
- Induction for SMT solvers
- Removing algebraic data types from constrained Horn clauses using difference predicates
- Automating induction by reflection
Describes a project that uses
Uses Software
This page was built for publication: Automating Induction with an SMT Solver
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2891425)
