Adding decision procedures to SMT solvers using axioms with triggers
From MaRDI portal
Publication:287384
DOI10.1007/S10817-015-9352-2zbMATH Open1356.68187OpenAlexW798190714MaRDI QIDQ287384FDOQ287384
Authors: Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich 
Publication date: 26 May 2016
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-015-9352-2
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
- Simplify: a theorem prover for program checking
- Booster: an acceleration-based verification framework for array programs
- Title not available (Why is that?)
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Title not available (Why is that?)
- A rewriting approach to satisfiability procedures.
- Deciding local theory extensions via E-matching
- Adding decision procedures to SMT solvers using axioms with triggers
- E-matching with free variables
- Correct code containing containers
- Towards Complete Reasoning about Axiomatic Specifications
- Sets with cardinality constraints in satisfiability modulo theories
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Engineering DPLL(T) + Saturation
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Efficient E-Matching for SMT Solvers
- Theory Instantiation
- Automatic decidability and combinability
- Computer Aided Verification
- Verification, Model Checking, and Abstract Interpretation
- Programming languages and systems. 9th Asian symposium, APLAS 2011, Kenting, Taiwan, December 5--7, 2011. Proceedings
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
Uses Software
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)
