Advertisement

Intra-module Inference

  • Shuvendu K. Lahiri
  • Shaz Qadeer
  • Juan P. Galeotti
  • Jan W. Voung
  • Thomas Wies
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)

Abstract

Contract-based property checkers hold the potential for precise, scalable, and incremental reasoning. However, it is difficult to apply such checkers to large program modules because they require programmers to provide detailed contracts, including an interface specification, module invariants, and internal specifications. We argue that given a suitably rich assertion language, modest effort suffices to document the interface specification and the module invariants. However, the burden of providing internal specifications is still significant and remains a deterrent to the use of contract-based checkers. Therefore, we consider the problem of intra-module inference, which aims to infer annotations for internal procedures and loops, given the interface specification and the module invariants. We provide simple and scalable techniques to search for a broad class of desired internal annotations, comprising quantifiers and Boolean connectives, guided by the module specification. We have validated our ideas by building a prototype verifier and using it to verify several properties on Windows device drivers with zero false alarms and small annotation overhead. These drivers are complex; they contain thousands of lines and use dynamic data structures such as linked lists and arrays. Our technique significantly improves the soundness, precision, and coverage of verification of these programs compared to earlier techniques.

Keywords

Public Procedure Device Driver Module Invariant Predicate Abstraction Internal Procedure 
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.
  2. 2.
    Aiken, A., Bugrara, S., Dillig, I., Dillig, T., Hackett, B., Hawkins, P.: An overview of the Saturn project. In: Program Analysis for Software Tools and Engineering (PASTE 2007), pp. 43–48. ACM, New York (2007) Google Scholar
  3. 3.
    Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: Programming Language Design and Implementation (PLDI 2001), pp. 203–213 (2001)Google Scholar
  4. 4.
    Barnett, M., Leino, K.R.M.: Weakest-precondition of unstructured programs. In: Program Analysis For Software Tools and Engineering (PASTE 2005), pp. 82–87. ACM, New York (2005)Google Scholar
  5. 5.
    Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  6. 6.
    Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamarić, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 19–33. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  7. 7.
    Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)Google Scholar
  8. 8.
    Condit, J., Hackett, B., Lahiri, S.K., Qadeer, S.: Unifying type checking and property checking for low-level code. In: Principles of Programming Languages (POPL 2009), pp. 302–314 (2009)Google Scholar
  9. 9.
    Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: Symposium on Principles of Programming Languages (POPL 1977), pp. 238–252. ACM Press, New York (1977)Google Scholar
  10. 10.
    Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: Programming Language Design and Implementation (PLDI 2002), pp. 57–68 (2002)Google Scholar
  11. 11.
    de Moura, L., Bjorner, N.: Efficient incremental e-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS, vol. 4603, pp. 183–198. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  12. 12.
    DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research (2005)Google Scholar
  13. 13.
    Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500–517. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  14. 14.
    Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Programming Language Design and Implementation (PLDI 2002), pp. 234–245 (2002)Google Scholar
  15. 15.
    Flanagan, C., Qadeer, S.: Predicate abstraction for software verification. In: Principles of Programming Languages (POPL 2002), pp. 191–202. ACM Press, New York (2002)Google Scholar
  16. 16.
    Graf, S., Saïdi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  17. 17.
    Gulwani, S., McCloskey, B., Tiwari, A.: Lifting abstract interpreters to quantified logical domains. In: Principles of Programming Languages (POPL 2008), pp. 235–246 (2008)Google Scholar
  18. 18.
    Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Principles of Programming Languages (POPL 2002), pp. 58–70 (2002)Google Scholar
  19. 19.
    Lahiri, S.K., Bryant, R.E.: Constructing quantified invariants via predicate abstraction. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 267–281. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  20. 20.
    Lahiri, S.K., Qadeer, S.: Back to the future: revisiting precise program verification using SMT solvers. In: Principles of Programming Languages (POPL 2008), pp. 171–182 (2008)Google Scholar
  21. 21.
    Lahiri, S.K., Qadeer, S.: Complexity and algorithms for monomial and clausal predicate abstraction. Technical Report MSR-TR-2009-2012, Microsoft Research (2009)Google Scholar
  22. 22.
    Lam, P., Kuncak, V., Rinard, M.C.: Generalized typestate checking for data structure consistency. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 430–447. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  23. 23.
    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
  24. 24.
    McMillan, K.L.: Quantified invariant generation using an interpolating saturation prover. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 413–427. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  25. 25.
    Sagiv, S., Reps, T.W., Wilhelm, R.: Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems (TOPLAS 1998) 20(1), 1–50 (1998)CrossRefGoogle Scholar
  26. 26.
    Yang, H., Lee, O., Berdine, J., Calcagno, C., Cook, B., Distefano, D., O’Hearn, P.W.: Scalable shape analysis for systems code. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 385–398. Springer, Heidelberg (2008)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Shuvendu K. Lahiri
    • 1
  • Shaz Qadeer
    • 1
  • Juan P. Galeotti
    • 2
  • Jan W. Voung
    • 3
  • Thomas Wies
    • 4
  1. 1.Microsoft ResearchUSA
  2. 2.University of Buenos AiresArgentina
  3. 3.University of CaliforniaSan Diego
  4. 4.École Polytechnique Fédérale de LausanneSwitzerland

Personalised recommendations