Adding decision procedures to SMT solvers using axioms with triggers
From MaRDI portal
(Redirected from Publication:287384)
Recommendations
- Extending SMT solvers to higher-order logic
- Extending Sledgehammer with SMT solvers
- Extending Sledgehammer with SMT solvers
- Induction for SMT solvers
- Automating Induction with an SMT Solver
- A decision procedure for (co)datatypes in SMT solvers
- A decision procedure for (co)datatypes in SMT solvers
- A decision procedure for separation logic in SMT
- scientific article; zbMATH DE number 1341612
Cites work
- scientific article; zbMATH DE number 5493266 (Why is no real title available?)
- scientific article; zbMATH DE number 3299786 (Why is no real title available?)
- A rewriting approach to satisfiability procedures.
- Adding decision procedures to SMT solvers using axioms with triggers
- Automatic decidability and combinability
- Booster: an acceleration-based verification framework for array programs
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Computer Aided Verification
- Correct code containing containers
- Deciding local theory extensions via E-matching
- E-matching with free variables
- Efficient E-Matching for SMT Solvers
- Engineering DPLL(T) + Saturation
- Programming languages and systems. 9th Asian symposium, APLAS 2011, Kenting, Taiwan, December 5--7, 2011. Proceedings
- Sets with cardinality constraints in satisfiability modulo theories
- Simplify: a theorem prover for program checking
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Theory Instantiation
- Towards Complete Reasoning about Axiomatic Specifications
- Verification, Model Checking, and Abstract Interpretation
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
Cited in
(7)- Triggerless happy. Intermediate verification with a first-order prover
- Metalevel algorithms for variant satisfiability
- Adding decision procedures to SMT solvers using axioms with triggers
- Axiomatic constraint systems for proof search modulo theories
- Instrumenting a weakest precondition calculus for counterexample generation
- Variant-Based Satisfiability in Initial Algebras
- Metalevel algorithms for variant satisfiability
This page was built for publication: Adding decision procedures to SMT solvers using axioms with triggers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q287384)
