What's New?

• Congratulations to the Driver Quality Team on winning a 2009 Engineering Excellence Award for "Improving Driver Quality thru Static Verification". Jon Hagen, Vlad Levin, Adam Shapiro, Donn Terry, Abdullah Ustuner. PREfast for Drivers scans the driver code for issues with concurrency, proper IRQL handling, and a host of other driver challenges. The Static Driver Verifier simulates a hostile environment and systematically tests all code paths, looking for driver model violations. These complementary tools provide both quick and deep driver testing. Both tools have been adopted broadly within Windows and with third-party developers through MSDN and the Windows Driver Kit.

• SLAM 2.0 has been transferred to the product group in charge of Static Driver Verifier, replacing the original SLAM engine.

• The Windows 7 Driver Kit beta is available.

• SLAM 2.0 uses the Z3 automated theorem prover and contains many advances.
• Yogi is a new abstraction-refinement engine based on test generation.
• Developing Drivers with the Windows® Driver Foundation, a Microsoft Press book, is now in print, including a chapter about Static Driver Verifier, which has new rules to enable analysis of drivers written against the Kernel-model Driver Framework API.

Downloads

• Get the Vista Windows Driver Kit (WDK), which includes Static Driver Verifier. Please follow these helpful directions to get the Vista WDK.
• Static Driver Verifier Rule Development Kit (RDK) for Vista WDK available
  • E-mail rdk_req@microsoft.com to request a copy of the RDK. You need to install the Vista WDK before installing the RDK. See above.
  • The RDK is an extension to Static Driver Verifier (SDV) that allows you to adapt SDV to support additional frameworks (or APIs) and write custom SLIC rules for this framework. The goal of the RDK is to allow researchers to experiment with writing SLIC rules for APIs and to gain experience using the SLAM verification engine that underlies SDV.

Papers

History

• SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft, T. Ball, B. Cook, V. Levin and S. K. Rajamani, Integrated Formal Methods 2004

The SLAM Process

• Thorough Static Analysis of Device Drivers, T. Ball, E. Bounimova, B. Cook, V. Levin, J. Lichtenberg, C. McGarvey, B. Ondrusek, S. K. Rajamani and A. Ustuner, EuroSys 2006
• The SLAM Project: Debugging System Software via Static Analysis, T. Ball, S. K. Rajamani, POPL 2002, January 2002, pages 1-3.
• Automatically Validating Temporal Safety Properties of Interfaces, T. Ball, S. K. Rajamani, SPIN 2001 Workshop on Model Checking of Software, LNCS 2057, May 2001, pp. 103-122.
• Checking Temporal Properties of Software with Boolean Programs, T. Ball, S. K. Rajamani, Workshop on Advances in Verification (with CAV 2000)
• Boolean Programs: A Model and Process for Software Analysis, T. Ball, S. K. Rajamani, MSR Technical Report 2000-14.

SLAM Specifications

• SLIC: A Specification Language for Interface Checking, T. Ball, S. K. Rajamani, MSR-TR-2001-21.

Boolean Programs

• Bebop: A Path-sensitive Interprocedural Dataflow Engine, T. Ball, S. K. Rajamani, PASTE 2001
• Bebop: A Symbolic Model Checker for Boolean Programs, T. Ball, S. K. Rajamani, SPIN 2000 Workshop on Model Checking of Software, LNCS 1885, August/September 2000, pp. 113-130.

• Predicate Abstraction of C Programs
  • Polymorphic Predicate Abstraction, T. Ball, T. Millstein, S. K. Rajamani, ACM TOPLAS Vol. 27, No. 2, March 2005, pages 314-343
  • Automatic Predicate Abstraction of C Programs, T. Ball, R. Majumdar, T. Millstein, S. K. Rajamani, PLDI 2001, SIGPLAN Notices 36(5), pp. 203-213.
  • Boolean and Cartesian Abstractions for Model Checking C Programs, T. Ball, A. Podelski, S. K. Rajamani, TACAS 2001, LNCS 2031, April 2001, pp. 268-283.
  • Predicate Abstraction via Symbolic Decision Procedures, S. Lahiri, T. Ball, B. Cook, CAV 2005.

Abstraction Refinement

• Refining Approximations in Software Predicate Abstraction, T. Ball, B. Cook, S. Das, S. K. Rajamani. TACAS 2004.
• Generating Abstract Explanations of Spurious Counterexamples in C Programs, T. Ball, S. K. Rajamani, MSR-TR-2002-09.
• Relative Completeness of Abstraction Refinement for Software Model Checking, T. Ball, A. Podelski, S. K. Rajamani, TACAS 2002, LNCS 2280, April 2002, pp. 158-172.
• Zapato: Automatic theorem proving for predicate abstraction refinement, T. Ball, B. Cook, S. K. Lahiri and L. Zhang, Tools paper in CAV 2004
• Formalizing Counterexample-driven Refinement with Weakest Preconditions, T. Ball, Proceedings of the NATO Advanced Study Institute on Engineering Theories of Software Intensive Systems Marktoberdorf, Germany 3–15 August 2004.

Concurrency

• Parameterized Verification of Multithreaded Software Libraries, T. Ball, S. Chaki, S. K. Rajamani,TACAS 2001, LNCS 2031, April 2001, pp. 158-173.

Miscellaneous

• From Symptom to Cause: Localizing Errors in Counterexample Traces, T. Ball, M. Naik, S. K. Rajamani, POPL 2003
• Speeding Up Dataflow Analysis Using Flow-Insensitive Pointer Analysis, S. Adams, T. Ball, M. Das, S. Lerner, S. K. Rajamani, M. Seigle, W. Weimer. SAS 2002, LNCS 2477
• Automatic Creation of Environment Models via Training, T. Ball, V. Levin, and F. Xie, TACAS 2004
• The SLAM Toolkit, T. Ball, S. K. Rajamani, CAV 2001

News

• Wired News: Microsoft's Secret Bug Squasher
• Kampf dem Programmierfehlerteufel
• SDV and PPRC tools mentioned in The Economist
• From reporting of the Microsoft Research Roadshow in Silicon Valley (PC Magazine)
• SLAM and PPRC tools featured in Bill Gates' OOPSLA 2002 keynote address

Related Projects

• Yogi is a new abstraction-refinment engine based on test generation.
• UC Berkeley's BLAST 1.0
• Sagar Chaki's MAGIC
• Stefan Schwoon's Moped
• Georg Weissenbacher's BOOP