Revisiting Enumerative Instantiation

Abstract : Formal methods applications often rely on SMT solvers to automatically discharge proof obligations. SMT solvers handle quantified formulas using incomplete heuristic techniques like E-matching, and often resort to model-based quantifier instantiation (MBQI) when these techniques fail. This paper revisits enumerative instantiation, a technique that considers instantiations based on exhaustive enumeration of ground terms. Although simple, we argue that enumer-ative instantiation can supplement other instantiation techniques and be a viable alternative to MBQI for valid proof obligations. We first present a stronger Her-brand Theorem, better suited as a basis for the instantiation loop used in SMT solvers; it furthermore requires considering less instances than classical Herbrand instantiation. Based on this result, we present different strategies for combining enumerative instantiation with other instantiation techniques in an effective way. The experimental evaluation shows that the implementation of these new techniques in the SMT solver CVC4 leads to significant improvements in several benchmark libraries, including many stemming from verification efforts.
Type de document :
Rapport
[Research Report] University of Iowa; Inria. 2018
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01744956
Contributeur : Haniel Barbosa <>
Soumis le : mardi 27 mars 2018 - 18:04:24
Dernière modification le : vendredi 30 mars 2018 - 01:26:59

Fichier

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

Identifiants

  • HAL Id : hal-01744956, version 1

Collections

Citation

Andrew Reynolds, Haniel Barbosa, Pascal Fontaine. Revisiting Enumerative Instantiation. [Research Report] University of Iowa; Inria. 2018. 〈hal-01744956〉

Partager

Métriques

Consultations de la notice

41

Téléchargements de fichiers

11