Localization and Register Sharing for Predicate Abstraction

  • Himanshu Jain
  • Franjo Ivančić
  • Aarti Gupta
  • Malay K. Ganai
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)


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.


Model Check Abstract Model Basic Block Boolean Variable Global Constraint 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Ball, T., Cook, B., Das, S., Rajamani, S.: Refining approximations in software predicate abstraction. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 388–403. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  2. 2.
    Ball, T., Majumdar, R., Millstein, T.D., Rajamani, S.K.: Automatic predicate abstraction of C programs. Programming Language Design and Implementation, 203–213 (2001)Google Scholar
  3. 3.
    Ball, T., Podelski, A., Rajamani, S.K.: Boolean and Cartesian abstraction for model checking C programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, p. 268. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: SPIN Workshop on Model Checking of Software. Springer, Heidelberg (2001)Google Scholar
  5. 5.
    Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. In: ICSE 2003, pp. 385–395. IEEE, Los Alamitos (2003)Google Scholar
  6. 6.
    Clarke, E., Kroening, D., Sharygina, N., Yorav, K.: Predicate abstraction of ANSI–C programs using SAT. Formal Methods in System Design 25, 105–127 (2004)zbMATHCrossRefGoogle Scholar
  7. 7.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, pp. 238–252 (1977)Google Scholar
  8. 8.
    Craig, W.: Linear reasoning. Journal of Symbolic Logic 22, 250–268 (1957)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Das, S., Dill, D., Park, S.: Experience with predicate abstraction. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 160–171. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  10. 10.
    Dijkstra, E.: A Discipline of Programming. Prentice Hall, Englewood Cliffs (1976)zbMATHGoogle Scholar
  11. 11.
    Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: CAV 1997, pp. 72–83. Springer, Heidelberg (1997)Google Scholar
  12. 12.
    Gupta, A., Ganai, M.K., Ashar, P., Yang, Z.: Iterative abstraction using SAT-based BMC with proof analysis. In: International Conference on Computer Aided Design (ICCAD) (2003)Google Scholar
  13. 13.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002, pp. 58–70 (2002)Google Scholar
  14. 14.
    Henzinger, T.A., Jhala, R., Majumdar, R., McMillan, K.L.: Abstractions from proofs. In: POPL 2004, pp. 232–244. ACM Press, New York (2004)CrossRefGoogle Scholar
  15. 15.
    Ivančić, F., Yang, Z., Ganai, M., Gupta, A., Ashar, P.: Efficient SAT-based bounded model checking for software verification. In: Symposium on Leveraging Applications of Formal Methods (2004)Google Scholar
  16. 16.
    Jain, H., Kroening, D., Clarke, E.: Verification of SpecC using predicate abstraction. In: MEMOCODE 2004, pp. 7–16. IEEE, Los Alamitos (2004)Google Scholar
  17. 17.
    Lahiri, S.K., Bryant, R.E., Cook, B.: A symbolic approach to predicate abstraction. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 141–153. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  18. 18.
    Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)Google Scholar
  19. 19.
    Rugina, R., Rinard, M.C.: Symbolic bounds analysis of pointers, array indices, and accessed memory regions. In: PLDI 2000, pp. 182–195 (2000)Google Scholar
  20. 20.
    Rusu, V., Singerman, E.: On proving safety properties by integrating static analysis, theorem proving and abstraction. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 178–192. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  21. 21.
    Zaks, A., Ivančić, F., Cadambi, H., Shlyakhter, I., Yang, Z., Ganai, M., Gupta, A., Ashar, P.: Range analysis for software verification (2005) (Submitted for publication)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Himanshu Jain
    • 1
  • Franjo Ivančić
    • 1
  • Aarti Gupta
    • 1
  • Malay K. Ganai
    • 1
  1. 1.NEC Laboratories AmericaPrinceton

Personalised recommendations