Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

20

CADE
2015
Springer

favoriteEmaildiscussreport

22views Logical Reasoning» more CADE 2015»

A Decision Procedure for (Co)datatypes in SMT Solvers

8 years 10 days ago

A Decision Procedure for (Co)datatypes in SMT Solvers

Download lara.epfl.ch

Abstract. We present a decision procedure that combines reasoning about datatypes and codatatypes. The dual of the acyclicity rule for datatypes is a uniqueness rule that identiﬁes observationally equal codatatype values, including cyclic values. The procedure decides universal problems and is composable via the Nelson–Oppen method. It has been implemented in CVC4, a state-of-the-art SMT solver. An evaluation based on problems generated from theories developed with Isabelle demonstrates the potential of the procedure.

Andrew Reynolds, Jasmin Christian Blanchette

Real-time Traffic

CADE 2015 | Logical Reasoning |

claim paper

Related Content

» On Using FloatingPoint Computations to Help an Exact Linear Arithmetic Decision Procedure

» Verifying HeapManipulating Programs in an SMT Framework

» Stochastic Local Search for SMT Combining Theory Solvers with WalkSAT

» Satisfiability Modulo the Theory of Costs Foundations and Applications

» A SliceBased Decision Procedure for TypeBased Partial Orders

» Generalized efficient array decision procedures

» TDecision by Decomposition

» Combination of Disjoint Theories Beyond Decidability

» Automatically Inferring Quantified Loop Invariants by Algorithmic Learning from Simple Tem...

» Interpolant Generation for UTVPI

Post Info
More Details (n/a)

Added	17 Apr 2016
Updated	17 Apr 2016
Type	Journal
Year	2015
Where	CADE
Authors	Andrew Reynolds, Jasmin Christian Blanchette

Comments (0)