A decision procedure for (co)datatypes in SMT solvers
From MaRDI portal
Publication:2360873
DOI10.1007/S10817-016-9372-6zbMATH Open1410.68337OpenAlexW2346936556MaRDI QIDQ2360873FDOQ2360873
Authors: Andrew Reynolds, Jasmin Christian Blanchette 
Publication date: 29 June 2017
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01643154/file/jour.pdf
Recommendations
Cites Work
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- Induction for SMT solvers
- Universal coalgebra: A theory of systems
- Isabelle/HOL. A proof assistant for higher-order logic
- Simplification by Cooperating Decision Procedures
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Results on the propositional \(\mu\)-calculus
- Extending Sledgehammer with SMT solvers
- A decision procedure for (co)datatypes in SMT solvers
- Efficient E-Matching for SMT Solvers
- Quantifier instantiation techniques for finite model finding in SMT
- Computer Aided Verification
- Combining nonstably infinite theories
- Theory of finite or infinite trees revisited
- A formally verified compiler back-end
- On equal \(\mu \)-terms
- Truly modular (co)datatypes for Isabelle/HOL
- Verifying a Compiler for Java Threads
- Combining superposition and induction: a practical realization
- On Rational Trees
- Model finding for recursive functions in SMT
- TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism
- An abstract decision procedure for a theory of inductive data types.
- Sharing is caring: combination of theories
- Witnessing (co)datatypes
Cited In (12)
- An abstract decision procedure for satisfiability in the theory of recursive data types
- Reasoning in the theory of heap: satisfiability and interpolation
- Witnessing (co)datatypes
- Adding decision procedures to SMT solvers using axioms with triggers
- SMTCoq: a plug-in for integrating SMT solvers into Coq
- Solving constrained Horn clauses over algebraic data types
- Title not available (Why is that?)
- Politeness for the theory of algebraic datatypes
- Datatypes with shared selectors
- A decision procedure for (co)datatypes in SMT solvers
- Reasoning about algebraic data types with abstractions
- Polite combination of algebraic datatypes
Uses Software
This page was built for publication: A decision procedure for (co)datatypes in SMT solvers
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2360873)
