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 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 language | English (US) |
---|---|
Pages (from-to) | 397-412 |
Number of pages | 16 |
Journal | LECTURE NOTES IN COMPUTER SCIENCE |
Volume | 3440 |
DOIs | |
State | Published - 2005 |
Event | 11th 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 2005 → Apr 8 2005 |
All Science Journal Classification (ASJC) codes
- Theoretical Computer Science
- General Computer Science