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~\cite{reynolds2014fmcad}. An enhanced version of the classical congruence closure algorithm, able to handle free variables, is presented.
Type de document :
Rapport
[Research Report] Inria Nancy - Grand Est (Villers-lès-Nancy, France). 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-01235912
Contributeur : Haniel Barbosa <>
Soumis le : lundi 30 novembre 2015 - 23:08:09
Dernière modification le : jeudi 22 septembre 2016 - 14:32:03
Document(s) archivé(s) le : mardi 1 mars 2016 - 16:20:56

Fichiers

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

Identifiants

  • HAL Id : hal-01235912, version 1

Collections

Citation

Haniel Barbosa, Pascal Fontaine. Congruence Closure with Free Variables (Work in Progress). [Research Report] Inria Nancy - Grand Est (Villers-lès-Nancy, France). 2015. 〈hal-01235912〉

Partager

Métriques

Consultations de la notice

87

Téléchargements de fichiers

34