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.
Type de document :
Communication dans un congrès
CADE-25, Aug 2015, Berlin, Germany. Lecture Notes in Computer Science, 2015, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. 〈10.1007/978-3-319-21401-6_13〉
Liste complète des métadonnées

Littérature citée [27 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01212585
Contributeur : Jasmin Christian Blanchette <>
Soumis le : mercredi 7 octobre 2015 - 15:22:30
Dernière modification le : lundi 20 novembre 2017 - 15:14:02
Document(s) archivé(s) le : vendredi 8 janvier 2016 - 10:15:43

Fichier

conf.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Andrew Reynolds, Jasmin Christian Blanchette. A Decision Procedure for (Co)datatypes in SMT Solvers. CADE-25, Aug 2015, Berlin, Germany. Lecture Notes in Computer Science, 2015, Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. 〈10.1007/978-3-319-21401-6_13〉. 〈hal-01212585〉

Partager

Métriques

Consultations de la notice

104

Téléchargements de fichiers

62