Tighter Integration of {BDDs} and {SMT} for Predicate Abstraction

Alessandro Cimatti 1 Anders Franzen 1 Alberto Griggio 2 Krishnamani Kalyanasundaram 1, 3 Marco Roveri 1
1 FBK - Fondazione Bruno Kessler [Trento, Italy]
2 DISI - Department of Information Engineering and Computer Science
3 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : We address the problem of computing the exact abstraction of a program with respect to a given set of predicates, a key computation step in Counter-Example Guided Abstraction Refinement. We build on a recently proposed approach that integrates BDD-based quantification techniques with SMT-based constraint solving to compute the abstraction. We extend the previous work in three main directions. First, we propose a much tighter integration of the BDD-based and SMT-based reasoning where the two solvers strongly collaborate to guide the search. Second, we propose a technique to reduce redundancy in the search by blocking already visited models. Third, we present an algorithm exploiting a conjunctively partitioned representation of the formula to quantify. This algorithm provides a general framework where all the presented optimizations integrate in a natural way. Moreover, it allows to overcome the limitations of the original approach that used a monolithic BDD representation of the formula to quantify. We experimentally evaluate the merits of the proposed optimizations, and show how they allow to significantly improve over previous approaches.
Type de document :
Communication dans un congrès
Design, Automation & Test in Europe, Mar 2010, Dresden, Germany. IEEE, pp.1707--1712, 2010
Liste complète des métadonnées
https://hal.inria.fr/inria-00535785
Contributeur : Claude Marché <>
Soumis le : vendredi 12 novembre 2010 - 17:07:33
Dernière modification le : jeudi 11 janvier 2018 - 06:22:14

Identifiants

  • HAL Id : inria-00535785, version 1

Collections

INRIA

Citation

Alessandro Cimatti, Anders Franzen, Alberto Griggio, Krishnamani Kalyanasundaram, Marco Roveri. Tighter Integration of {BDDs} and {SMT} for Predicate Abstraction. Design, Automation & Test in Europe, Mar 2010, Dresden, Germany. IEEE, pp.1707--1712, 2010. 〈inria-00535785〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

154

Contact


archive-ouverte@inria.fr