Skip to Main content Skip to Navigation
Conference papers

A Decision Procedure for (Co)datatypes in SMT Solvers

Andrew Reynolds 1 Jasmin Blanchette 2, 3
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [5 references]  Display  Hide  Download
Contributor : Jasmin Blanchette Connect in order to contact the contributor
Submitted on : Tuesday, November 15, 2016 - 2:15:02 PM
Last modification on : Wednesday, November 3, 2021 - 7:10:16 AM
Long-term archiving on: : Thursday, March 16, 2017 - 5:23:53 PM


Files produced by the author(s)


  • HAL Id : hal-01397082, version 1



Andrew Reynolds, Jasmin Blanchette. A Decision Procedure for (Co)datatypes in SMT Solvers. IJCAI 2016 - 25th International Joint Conference on Artificial Intelligence, Jul 2016, New York, United States. ⟨hal-01397082⟩



Les métriques sont temporairement indisponibles