Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
SLAM

SLAM is a project for checking that software satisfies critical behavioral properties of the interfaces it uses and to aid software engineers in designing interfaces and software that ensure reliable and correct functioning. Static Driver Verifier is a tool in the Windows Driver Development Kit that uses the SLAM verification engine.

What's New?

  • Yogi is now available to plug into the Static Driver Verifier Research Platform. To install SDVRP and Yogi, see this README.
  • The Summer (2011) of SLAM saw two awards and a retrospective article in CACM:
  • Paper:
  • The Static Driver Verifier Research Platform (SDVRP) is a release of SDV/SLAM for academic research. It allows the creation and checking of API-specific rules and programs (for general APIs and programs, not just driver APIs and drivers) and contains a repository of Boolean programs and test results.
  • Pointers in SLAM2. Efficient evaluation of pointer predicates with Z3 SMT Solver in SLAM2, Thomas Ball, Ella Bounimova, Vladimir Levin, Leonardo de Moura, March 2010, MSR-TR-2010-24
  • 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.

Publications

Book Chapter

History

The SLAM Process

SLAM Specifications

Boolean Programs

Abstraction Refinement

Concurrency

Miscellaneous

 

News

 

Related Projects

People

"Things like even software verification, this has been the Holy Grail of computer science for many decades but now in some very key areas, for example, driver verification we’re building tools that can do actual proof about the software and how it works in order to guarantee the reliability." Bill Gates, April 18, 2002. Keynote address at WinHec 2002