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...

• Type: Conference
• Year: 2005
• Where: TACAS
• Authors: Himanshu Jain, Franjo Ivancic, Aarti Gupta, Malay K. Ganai
• Keywords: Abstraction, Abstraction Refinement, Algorithms, Predicate Abstraction, TACAS 2005