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.
See also
- Abstraction model checking
- the BLAST model checker, a model checker similar to SLAM that uses "lazy abstraction"
External links
|
|
|
|---|---|
| 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 |
| Others | MyLifeBits · LiveStation · Terminator |
| Operating system | Singularity |
| APIs | Joins · Accelerator · Dryad · SXM |
| Launched as products | C# · F# · Sideshow · Surface (TouchLight) · SenseCam · ClearType · Group Shot · Allegiance |
