Sciweavers

Share
CAV
2006
Springer

SMT Techniques for Fast Predicate Abstraction

8 years 11 months ago
SMT Techniques for Fast Predicate Abstraction
niques for Fast Predicate Abstraction Shuvendu K. Lahiri , Robert Nieuwenhuis , and Albert Oliveras Abstract. Predicate abstraction is a technique for automatically exfinite-state abstractions for systems with potentially infinite ace. The fundamental operation in predicate abstraction is to compute the best approximation of a Boolean formula over a set of predicates P. In this work, we demonstrate the use for this operation of a decision procedure based on the DPLL(T) framework for SAT Modulo Theories (SMT). The new algorithm is based on a careful generation of the set of all satisfying assignments over a set of predicates. It consistently outperforms previous methods by a factor of at least 20, on a diverse set of hardware and software verification benchmarks. We report detailed analysis of the results and the impact of a number of variations of the techniques. We also propose and evaluate a scheme for incremennement of approximations for predicate abstraction in the above framework...
Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oli
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CAV
Authors Shuvendu K. Lahiri, Robert Nieuwenhuis, Albert Oliveras
Comments (0)
books