| HAL-Inria | Publications, software ... of Inria's scientists |
Journal articles
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 formalizations developed with Isabelle demonstrates the potential of the procedure.
Cited literature [40 references]
https://hal.inria.fr/hal-01643154
Contributor : Jasmin Blanchette <>
Submitted on : Tuesday, November 21, 2017 - 10:36:25 AM
Last modification on : Monday, July 16, 2018 - 6:36:03 PM
Contributor : Jasmin Blanchette <>
Submitted on : Tuesday, November 21, 2017 - 10:36:25 AM
Last modification on : Monday, July 16, 2018 - 6:36:03 PM
File
jour.pdf
Files produced by the author(s)