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.
Type de document :
Article dans une revue
Journal of Automated Reasoning, Springer Verlag, 2017, 58 (3), pp.341 - 362. 〈10.1007/s10817-016-9372-6〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01643154
Contributeur : Jasmin Christian Blanchette <>
Soumis le : mardi 21 novembre 2017 - 10:36:25
Dernière modification le : lundi 16 juillet 2018 - 18:36:03

Fichier

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

Identifiants

Citation

Andrew Reynolds, Jasmin Christian Blanchette. A Decision Procedure for (Co)datatypes in SMT Solvers. Journal of Automated Reasoning, Springer Verlag, 2017, 58 (3), pp.341 - 362. 〈10.1007/s10817-016-9372-6〉. 〈hal-01643154〉

Partager

Métriques

Consultations de la notice

130

Téléchargements de fichiers

24