Sciweavers

Share
TACAS
2005
Springer

Localization and Register Sharing for Predicate Abstraction

11 years 5 months ago
Localization and Register Sharing for Predicate Abstraction
ion Himanshu Jain1,2 , Franjo Ivanˇci´c1 , Aarti Gupta1 , and Malay K. Ganai1 1 NEC Laboratories America, Inc., 4 Independence Way, Princeton, NJ 08540 2 School of Computer Science, Carnegie Mellon University, Pittsburgh, PA Abstract. In the domain of software verification, predicate abstraction has emerged to be a powerful and popular technique for extracting finite-state models from often complex source code. In this paper, we report on the application of three techniques for improving the performance of the predicate abstraction ret loop. The first technique allows faster computation of the abstraction. Instead of maintaining a global set of predicates, we find predicates relevant to various basic blocks of the program by weakest pre-condition propagation along spurious program traces. The second technique enables faster model checking of raction by reducing the number of state variables in the abstraction. This is done by re-using Boolean variables to represent different pred...
Himanshu Jain, Franjo Ivancic, Aarti Gupta, Malay
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TACAS
Authors Himanshu Jain, Franjo Ivancic, Aarti Gupta, Malay K. Ganai
Comments (0)
books