Adding decision procedures to SMT solvers using axioms with triggers
From MaRDI portal
Publication:287384
DOI10.1007/s10817-015-9352-2zbMath1356.68187OpenAlexW798190714MaRDI QIDQ287384
Sylvain Conchon, Claire Dross, 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
Related Items
Adding decision procedures to SMT solvers using axioms with triggers, Instrumenting a weakest precondition calculus for counterexample generation, Metalevel algorithms for variant satisfiability, Axiomatic Constraint Systems for Proof Search Modulo Theories, Variant-Based Satisfiability in Initial Algebras, Metalevel Algorithms for Variant Satisfiability
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Adding decision procedures to SMT solvers using axioms with triggers
- Automatic decidability and combinability
- Programming languages and systems. 9th Asian symposium, APLAS 2011, Kenting, Taiwan, December 5--7, 2011. Proceedings
- A rewriting approach to satisfiability procedures.
- Deciding local theory extensions via E-matching
- E-Matching with Free Variables
- Correct Code Containing Containers
- Towards Complete Reasoning about Axiomatic Specifications
- Sets with Cardinality Constraints in Satisfiability Modulo Theories
- Solving SAT and SAT Modulo Theories
- Booster: An Acceleration-Based Verification Framework for Array Programs
- iProver – An Instantiation-Based Theorem Prover for First-Order Logic (System Description)
- Engineering DPLL(T) + Saturation
- Simplify: a theorem prover for program checking
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Efficient E-Matching for SMT Solvers
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Theory Instantiation
- Computer Aided Verification
- Verification, Model Checking, and Abstract Interpretation
