SLAM project

From Wikipedia, the free encyclopedia

The SLAM project, which is started in Microsoft Research, aimed for verifying some software properties using model checking techniques. It is implemented in Ocaml, and has been used to find many bugs in Windows Device Drivers. It is distributed as part of the Microsoft Windows Driver Foundation development kit as the Static Driver Verifier (SDV).

SLAM uses a technique called counterexample-guided abstraction refinement, which uses progressively better models of the program under test to verify.

[edit] See also

• Abstraction model checking
• the BLAST model checker, a model checker similar to SLAM that uses "lazy abstraction"

[edit] External links

• SLAM website

v • d • e Microsoft Research (MSR) Languages and compilers Polyphonic C# · Cω · Spec# · Sing# · Bartok · Phoenix Distributed / grid computing Bigtop · Gridline · BitVault Internet and networking Avalanche · Wallop · Conference XP · HoneyMonkey · AjaxView Other projects MyLifeBits · LiveStation · Terminator · WorldWide Telescope Operating systems Singularity APIs Joins · Accelerator · Dryad  · SXM Launched as products C# · Comic Chat · F# · Sideshow · Surface (TouchLight) · SenseCam · ClearType · Group Shot · Allegiance