Advertisement

Automatically Refining Abstract Interpretations

  • Bhargav S. Gulavani
  • Supratik Chakraborty
  • Aditya V. Nori
  • Sriram K. Rajamani
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4963)

Abstract

Abstract interpretation techniques prove properties of programs by computing abstract fixpoints. All such analyses suffer from the possibility of false errors. We present three techniques to automatically refine such abstract interpretations to reduce false errors: (1) a new operator called interpolated widen, which automatically recovers precision lost due to widen, (2) a new way to handle disjunctions that arise due to refinement, and (3) a new refinement algorithm, which refines abstract interpretations that use the join operator to merge abstract states at join points. We have implemented our techniques in a tool Dagger. Our experimental results show our techniques are effective and that their combination is even more effective than any one of them in isolation. We also show that Dagger is able to prove properties of C programs that are beyond current abstraction-refinement tools, such as Slam [4], Blast [15], Armc [19], and our earlier tool [12].

Keywords

Abstract State Abstract Interpretation Abstract Domain Base Exploration Predicate Abstraction 
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.

References

  1. 1.
    Apron. Numerical Abstract Domain Library, http://apron.cri.ensmp.fr/library/
  2. 2.
    Bagnara, R., Hill, P., Zaffanella, E.: Widening operators for powerset domains. Technical Report 344, University of Parma, Italy (2004)Google Scholar
  3. 3.
    Bagnara, R., Hill, P.M., Ricci, E., Zaffanella, E.: Precise widening opertors for convex polyhedra. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, Springer, Heidelberg (2003)CrossRefGoogle Scholar
  4. 4.
    Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL 2002, pp. 1–3 (2002)Google Scholar
  5. 5.
    Beyer, D., Henzinger, T.A., Majumdar, R., Rybalchenko, A.: Path invariants. In: PLDI, pp. 300–309 (2007)Google Scholar
  6. 6.
    CIL. Infrastructure for C Program Analysis and Transformation. http://manju.cs.berkeley.edu/cil/
  7. 7.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238–252 (1977)Google Scholar
  8. 8.
    Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with craig interpolation and symbolic pushdown systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 489–503. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  9. 9.
    Fischer, J., Jhala, R., Majumdar, R.: Joining dataflow with predicates. In: ESEC/SIGSOFT FSE, pp. 227–236 (2005)Google Scholar
  10. 10.
    Gopan, D., Reps, T.W.: Lookahead widening. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 452–466. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  11. 11.
    B. S. Gulavani, S. Chakraborty, A. V. Nori, and S. K. Rajamani. Automatically refining abstract interpretations. Technical Report TR-07-23, CFDVS, IIT Bombay, 2007. http://www.cfdvs.iitb.ac.in/~bhargav/dagger.html
  12. 12.
    Gulavani, B.S., Rajamani, S.K.: Counterexample driven refinement for abstract interpretation. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 474–488. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  13. 13.
    Halbwachs, N., Proy, Y.E., Roumanoff, P.: Verification of real-time systems using linear relation analysis. FMSD 11(2), 157–185 (1997)CrossRefGoogle Scholar
  14. 14.
    Henzinger, T., Jhala, R., Majumdar, R., McMillan, K.: Abstractions from proofs. In: POPL (2004)Google Scholar
  15. 15.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58–70 (2002)Google Scholar
  16. 16.
    Jain, H., Ivancic, F., Gupta, A., Shlyakhter, I., Wang, C.: Using statically computed invariants inside the predicate abstraction and refinement loop. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 137–151. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  17. 17.
    Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  18. 18.
    McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  19. 19.
    Rybalchenko, A., Podelski, A.: Armc: The logical choice for software model checking with abstraction refinement. In: PADL (2007)Google Scholar
  20. 20.
    Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint solving for interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 346–362. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  21. 21.
    Sankaranarayanan, S., Sipma, H., Manna, Z.: Constraint based linear-relations analysis. In: Giacobazzi, R. (ed.) SAS 2004. LNCS, vol. 3148, pp. 53–68. Springer, Heidelberg (2004)Google Scholar
  22. 22.
    Wang, C., Yang, Z., Gupta, A., Ivancic, F.: Using counterexamples for improving the precision of reachability computation with polyhedra. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 352–365. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  23. 23.
    Zitser, M., Lippmann, R., Leek, T.: Testing static analysis tools using exploitable buffer overflows from open source code. In: FSE, pp. 97–106 (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Bhargav S. Gulavani
    • 1
  • Supratik Chakraborty
    • 1
  • Aditya V. Nori
    • 2
  • Sriram K. Rajamani
    • 2
  1. 1.IITBombay
  2. 2.Microsoft ResearchIndia

Personalised recommendations