A Decision Procedure for (Co)datatypes in SMT Solvers

DOI10.1007/978-3-319-21401-6_13zbMath1465.68297OpenAlexW1441804354MaRDI QIDQ3454092

Andrew Reynolds, Jasmin Christian Blanchette

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-21401-6_13

Mathematics Subject Classification ID

Abstract data types; algebraic specification (68Q65) Decidability of theories and sets of sentences (03B25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (4)

A decision procedure for (co)datatypes in SMT solvers ⋮ A Decision Procedure for (Co)datatypes in SMT Solvers ⋮ Syntax-guided quantifier instantiation ⋮ Model Finding for Recursive Functions in SMT

Uses Software

• Nitpick
• z3
• Sledgehammer
• StarExec
• CVC4
• RADA

Cites Work

• Unnamed Item
• Results on the propositional \(\mu\)-calculus
• Universal coalgebra: A theory of systems
• Extending Sledgehammer with SMT solvers
• A formally verified compiler back-end
• Combining Superposition and Induction: A Practical Realization
• Sharing Is Caring: Combination of Theories
• A Decision Procedure for (Co)datatypes in SMT Solvers
• Theory of finite or infinite trees revisited
• Verifying a Compiler for Java Threads
• Efficient E-Matching for SMT Solvers
• On Rational Trees
• Simplification by Cooperating Decision Procedures
• Quantifier Instantiation Techniques for Finite Model Finding in SMT
• Induction for SMT Solvers
• Computer Aided Verification
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder

This page was built for publication: A Decision Procedure for (Co)datatypes in SMT Solvers