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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
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)
Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic theorem proving for predicate abstraction refinement. Under review (2004)
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)
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)
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)
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)
Ball, T., Millstein, T., Rajamani, S.K.: Polymorphic predicate abstraction. Technical Report MSR-TR-2001-10, Microsoft Research (2001)
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)
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)
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)
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)
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)
Ball, T., Rajamani, S.K.: Boolean programs: A model and process for software analysis. Technical Report MSR-TR-2000-14, Microsoft Research (January 2000)
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)
Ball, T., Rajamani, S.K.: SLIC: A specification language for interface checking. Technical Report MSR-TR-2001-21, Microsoft Research (2001)
Ball, T., Rajamani, S.K.: Generating abstract explanations of spurious counterexamples in C programs. Technical Report MSR-TR-2002-09, Microsoft Research (January 2002)
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)
Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers C-35(8), 677–691 (1986)
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)
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)
Chailloux, E., Manoury, P., Pagano, B.: Dévelopment d’Applications. Avec Objective CAML, O’Reilly, Paris
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)
Das, M.: Unification-based pointer analysis with directional assignments. In: PLDI 2000: Programming Language Design and Implementation, pp. 35–46. ACM, New York (2000)
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)
DeLine, R., Fähndrich, M.: The Fugue protocol checker: Is your software baroque? Technical Report MSR-TR-2004-07, Microsoft Research (2004)
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)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Labs (2003)
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)
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)
Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL 2002, January 2002, pp. 58–70. ACM, New York (2002)
Kurshan, R.P.: Computer-aided Verification of Coordinating Processes. Princeton University Press, Princeton (1994)
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)
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)
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)
Somenzi, F.: Colorado university decision diagram package, Technical Report available from ftp://vlsi.colorado.edu/pub University of Colorado, Boulder(1998)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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