SLAM and static driver verifier: Technology transfer of formal methods inside microsoft

172Citations
Citations of this article
88Readers
Mendeley users who have this article in their library.
Get full text

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. © Springer-Verlag 2004.

Cite

CITATION STYLE

APA

Ball, T., Cook, B., Levin, V., & Sriram, K. (2004). SLAM and static driver verifier: Technology transfer of formal methods inside microsoft. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2999, 1–20. https://doi.org/10.1007/978-3-540-24756-2_1

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free