Skip to main content
SpringerLink
Log in

SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft

  • Conference paper
Integrated Formal Methods (IFM 2004)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2999))

Included in the following conference series:

Abstract

The SLAM project originated in Microsoft Research in early 2000. Its goal was to automatically check that a C program correctly uses the interface to an external library. The project used and extended ideas from symbolic model checking, program analysis and theorem proving in novel ways to address this problem. The SLAM analysis engine forms the core of a new tool called Static Driver Verifier (SDV) that systematically analyzes the source code of Windows device drivers against a set of rules that define what it means for a device driver to properly interact with the Windows operating system kernel.

We believe that the history of the SLAM project and SDV is an informative tale of the technology transfer of formal methods and software tools. We discuss the context in which the SLAM project took place, the first two years of research on the SLAM project, the creation of the SDV tool and its transfer to the Windows development organization. In doing so, we call out many of the basic ingredients we believe to be essential to technology transfer: the choice of a critical problem domain; standing on the shoulders of those who have come before; the establishment of relationships with “champions” in product groups; leveraging diversity in research and development experience and careful planning and honest assessment of progress towards goals.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Adams, S., Ball, T., Das, M., Lerner, S., Rajamani, S.K., Seigle, M., Weimer, W.: Speeding up dataflow analysis using flow-insensitive pointer analysis. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 230–246. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  2. Ball, T., Cook, B., Das, S., Rajamani, S.K.: Refining approximations in software predicate abstraction. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 388–403. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  3. Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic theorem proving for predicate abstraction refinement. Under review (2004)

    Google Scholar 

  4. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Information and Computation 98(2), 142–170 (1992)

    Article  MATH  MathSciNet  Google Scholar 

  5. Ball, T., Chaki, S., Rajamani, S.K.: Parameterized verification of multithreaded software libraries. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, Springer, Heidelberg (2001)

    Google Scholar 

  6. Ball, T., Levin, V., Xei, F.: Automatic creation of environment models via training. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 93–107. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. In: PLDI 2001: Programming Language Design and Implementation, pp. 203–213. ACM, New York (2001)

    Chapter  Google Scholar 

  8. Ball, T., Millstein, T., Rajamani, S.K.: Polymorphic predicate abstraction. Technical Report MSR-TR-2001-10, Microsoft Research (2001)

    Google Scholar 

  9. Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: Localizing errors in counterexample traces. In: POPL 2003: Principles of programming languages, pp. 97–105. ACM, New York (2003)

    Google Scholar 

  10. Ball, T., Podelski, A., Rajamani, S.K.: Boolean and cartesian abstractions for model checking C programs. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 268–283. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  11. Ball, T., Podelski, A., Rajamani, S.K.: On the relative completeness of abstraction refinement. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 158–172. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  12. Bush, W.R., Pincus, J.D., Sielaff, D.J.: A static analyzer for finding dynamic programming errors. Software-Practice and Experience 30(7), 775–802 (2000)

    Article  MATH  Google Scholar 

  13. Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for Boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 113–130. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  14. Ball, T., Rajamani, S.K.: Boolean programs: A model and process for software analysis. Technical Report MSR-TR-2000-14, Microsoft Research (January 2000)

    Google Scholar 

  15. Ball, T., Rajamani, S.K.: Bebop: A path-sensitive interprocedural dataflow engine. In: PASTE 2001: Workshop on Program Analysis for Software Tools and Engineering, pp. 97–103. ACM, New York (2001)

    Chapter  Google Scholar 

  16. Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking. Technical Report MSR-TR-2001-21, Microsoft Research (2001)

    Google Scholar 

  17. Ball, T., Rajamani, S.K.: Generating abstract explanations of spurious counterexamples in C programs. Technical Report MSR-TR-2002-09, Microsoft Research (January 2002)

    Google Scholar 

  18. Ball, T., Rajamani, S.K.: The SLAM project: Debugging system software via static analysis. In: POPL 2002: Principles of Programming Languages, January 2002, pp. 1–3. ACM, New York (2002)

    Google Scholar 

  19. Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)

    Article  Google Scholar 

  20. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for the static analysis of programs by construction or approximation of fixpoints. In: POPL 1977: Principles of Programming Languages, pp. 238–252. ACM, New York (1977)

    Google Scholar 

  21. Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in c. In: ICSE 2003: International Conference on Software Engineering, pp. 385–395. ACM, New York (2003)

    Google Scholar 

  22. Chailloux, E., Manoury, P., Pagano, B.: Dévelopment d’Applications. Avec Objective CAML, O’Reilly, Paris

    Google Scholar 

  23. Chou, A., Yang, J., Chelf, B., Hallem, S., Engler, D.: An empirical study of operating systems errors. In: SOSP 2001: Symposium on Operating System Principles, pp. 73–88. ACM, New York (2001)

    Chapter  Google Scholar 

  24. Das, M.: Unification-based pointer analysis with directional assignments. In: PLDI 2000: Programming Language Design and Implementation, pp. 35–46. ACM, New York (2000)

    Chapter  Google Scholar 

  25. DeLine, R., Fähndrich, M.: Enforcing high-level protocols in low-level software. In: PLDI 2001: Programming Language Design and Implementation, pp. 59–69. ACM, New York (2001)

    Chapter  Google Scholar 

  26. DeLine, R., Fähndrich, M.: The Fugue protocol checker: Is your software baroque? Technical Report MSR-TR-2004-07, Microsoft Research (2004)

    Google Scholar 

  27. Das, M., Lerner, S., Seigle, M.: ESP: Path-sensitive program verification in polynomial time. In: PLDI 2002: Programming Language Design and Implementation, June 2002, pp. 57–68. ACM, New York (2002)

    Chapter  Google Scholar 

  28. Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (2003)

    Google Scholar 

  29. Esparza, J., Schwoon, S.: A bdd-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 324–336. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  30. 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)

    Google Scholar 

  31. Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002, January 2002, pp. 58–70. ACM, New York (2002)

    Chapter  Google Scholar 

  32. Kurshan, R.P.: Computer-aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)

    Google Scholar 

  33. Larus, J.R., Ball, T., Das, M., DeLine, R., Fähndrich, M., Pincus, J., Rajamani, S.K., Venkatapathy, R.: Righting software. IEEE Software (2004) (to appear)

    Google Scholar 

  34. Leino, K.R.M.: A sat characterization of boolean-program correctness. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 104–120. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  35. Reps, T., Horwitz, S., Sagiv, M.: Precise interprocedural dataflow analysis via graph reachability. In: POPL 1995: Principles of Programming Languages, pp. 49–61. ACM, New York (1995)

    Google Scholar 

  36. Somenzi, F.: Colorado university decision diagram package, Technical Report available from ftp://vlsi.colorado.edu/pub University of Colorado, Boulder(1998)

  37. Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, pp. 189–233. Prentice-Hall, Englewood Cliffs (1981)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Microsoft Corporation,  

    Thomas Ball, Byron Cook, Vladimir Levin & Sriram K. Rajamani

Authors
  1. Thomas Ball
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Byron Cook
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Vladimir Levin
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Sriram K. Rajamani
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, University of Kent, CT2 7NF, Canterbury, Kent, UK

    Eerke A. Boiten

  2. Department of Computing, University of Sheffield, S1 4DP, Sheffield, UK

    John Derrick

  3. School of Information Technology and Electrical Engineering, The University of Queensland, 4072, Australia

    Graeme Smith

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ball, T., Cook, B., Levin, V., Rajamani, S.K. (2004). SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G. (eds) Integrated Formal Methods. IFM 2004. Lecture Notes in Computer Science, vol 2999. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24756-2_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24756-2_1

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-21377-2

  • Online ISBN: 978-3-540-24756-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation