Skip to Main content Skip to Navigation
Conference papers

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 
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.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/inria-00535785
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Friday, November 12, 2010 - 5:07:33 PM
Last modification on : Friday, February 4, 2022 - 3:22:51 AM

Identifiers

  • HAL Id : inria-00535785, version 1

Collections

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. pp.1707--1712. ⟨inria-00535785⟩

Share

Metrics

Record views

77