| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
A Decision Procedure for (Co)datatypes in SMT Solvers
Abstract : Datatypes and codatatypes are useful to represent finite and potentially infinite objects. We describe a decision procedure to reason about such types. The procedure has been integrated into CVC4, a modern SMT (satisfiability modulo theories) solver, which can be used both as a constraint solver and as an automatic theorem prover. An evaluation based on formalizations developed in the Isabelle proof assistant shows the potential of the procedure.
Cited literature [5 references]
https://hal.inria.fr/hal-01397082
Contributor : Jasmin Blanchette <>
Submitted on : Tuesday, November 15, 2016 - 2:15:02 PM
Last modification on : Friday, December 11, 2020 - 6:44:56 PM
Long-term archiving on: : Thursday, March 16, 2017 - 5:23:53 PM
Contributor : Jasmin Blanchette <>
Submitted on : Tuesday, November 15, 2016 - 2:15:02 PM
Last modification on : Friday, December 11, 2020 - 6:44:56 PM
Long-term archiving on: : Thursday, March 16, 2017 - 5:23:53 PM
File
sister.pdf
Files produced by the author(s)