Sciweavers

Share
CADE
2015
Springer

A Decision Procedure for (Co)datatypes in SMT Solvers

4 years 2 months ago
A Decision Procedure for (Co)datatypes in SMT Solvers
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 identifies 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
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CADE
Authors Andrew Reynolds, Jasmin Christian Blanchette
Comments (0)
books