Localization and register sharing for predicate abstraction

Himanshu Jain, Franjo Ivančić, Aarti Gupta, Malay K. Ganai

Research output: Contribution to journalConference articlepeer-review

17 Scopus citations


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 refinement 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 the abstraction by reducing the number of state variables in the abstraction. This is done by re-using Boolean variables to represent different predicates in the abstraction. However, some predicates are useful at many program locations and discovering them lazily in various parts of the program leads to a large number of abstraction refinement iterations. The third technique attempts to identify such predicates early in the abstraction refinement loop and handles them separately by introducing dedicated state variables for such predicates. We have incorporated these techniques into NEC's software verification tool F-SoFT, and present promising experimental results for various case studies using these techniques.

Original languageEnglish (US)
Pages (from-to)397-412
Number of pages16
StatePublished - Sep 19 2005
Event11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 - Edinburgh, United Kingdom
Duration: Apr 4 2005Apr 8 2005

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)


Dive into the research topics of 'Localization and register sharing for predicate abstraction'. Together they form a unique fingerprint.

Cite this