A Decision Procedure for (Co)datatypes in SMT Solvers

Andrew Reynolds; Jasmin Blanchette

A Decision Procedure for (Co)datatypes in SMT Solvers

Andrew Reynolds ¹ Jasmin Blanchette ^{2, 3, 4}

1 University of Iowa [Iowa City]

2 Inria - Institut National de Recherche en Informatique et en Automatique

3 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems

Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods

4 MPII - Max-Planck-Institut für Informatik

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.

Type de document :

Communication dans un congrès

IJCAI 2016, Jul 2016, New York City, United States. Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016

Domaine :

Informatique [cs] / Logique en informatique [cs.LO]

Liste complète des métadonnées

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

https://hal.inria.fr/hal-01397082
Contributeur : Jasmin Christian Blanchette <>
Soumis le : mardi 15 novembre 2016 - 14:15:02
Dernière modification le : mardi 18 décembre 2018 - 16:38:25
Document(s) archivé(s) le : jeudi 16 mars 2017 - 17:23:53

sister.pdf

Fichiers produits par l'(les) auteur(s)

A Decision Procedure for (Co)datatypes in SMT Solvers

Fichier

Identifiants

Collections

Citation

Exporter

Métriques

140

58

Contact

A Decision Procedure for (Co)datatypes in SMT Solvers

Fichier

Identifiants

Collections

Citation

Exporter

Partager

Métriques

140

58

Contact