Congruence Closure with Free Variables (Work in Progress)

Haniel Barbosa 1 Pascal Fontaine 1
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : This paper presents preliminary work on the definition of a general framework for handling quantified formulas in SMT solving. Its focus is on the derivation of instances conflicting with a ground context, redefining the approach introduced in [11]. An enhanced version of the classical congruence closure algorithm, able to handle free variables, is presented.
Type de document :
Communication dans un congrès
Quantify 2015 : 2nd International Workshop on Quantification, 2015, Berlin, Germany. 2015
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01246036
Contributeur : Pascal Fontaine <>
Soumis le : vendredi 18 décembre 2015 - 10:21:58
Dernière modification le : jeudi 22 septembre 2016 - 14:31:53
Document(s) archivé(s) le : samedi 29 avril 2017 - 20:37:22

Fichier

BarbosaFontaine-QUANTIFY2015.p...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01246036, version 1

Collections

Citation

Haniel Barbosa, Pascal Fontaine. Congruence Closure with Free Variables (Work in Progress). Quantify 2015 : 2nd International Workshop on Quantification, 2015, Berlin, Germany. 2015. 〈hal-01246036〉

Partager

Métriques

Consultations de la notice

128

Téléchargements de fichiers

37