SLAM project
Encyclopedia
The SLAM project, which was started by Microsoft Research
, aimed at verifying some software safety 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.
"SLAM originally was an acronym but we found it too cumbersome to explain. We now prefer to think of 'slamming' the bugs in a program."Ball, Thomas; Cook, Byron; Levin, Vladimir; and Rajamani, Sriram K.; [ftp://ftp.research.microsoft.com/pub/tr/tr-2004-08.pdf SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft]; Lecture Notes in Computer Science (LNCS), Vol. 2999: Boiten, Eerke A.; Derrick, John; and Smith, Graeme; eds.; Fourth International Conference on Integrated Formal Methods (IFM 2004), 4–7 April 2004, Canterbury, GB, Springer, Berlin/Heidelberg, pp. 1–20 It probably stood for "Software, Languages, Analysis, and Modeling." Note that Microsoft has since re-used SLAM to stand for "Social Location Annotation Mobile".
Microsoft Research
Microsoft Research is the research division of Microsoft created in 1991 for developing various computer science ideas and integrating them into Microsoft products. It currently employs Turing Award winners C.A.R. Hoare, Butler Lampson, and Charles P...
, aimed at verifying some software safety properties using model checking
Model checking
In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....
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
Windows Driver Foundation
Windows Driver Foundation is a set of Microsoft tools that aid in the creation of device drivers for Windows 2000 and later versions of Windows....
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.
"SLAM originally was an acronym but we found it too cumbersome to explain. We now prefer to think of 'slamming' the bugs in a program."Ball, Thomas; Cook, Byron; Levin, Vladimir; and Rajamani, Sriram K.; [ftp://ftp.research.microsoft.com/pub/tr/tr-2004-08.pdf SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft]; Lecture Notes in Computer Science (LNCS), Vol. 2999: Boiten, Eerke A.; Derrick, John; and Smith, Graeme; eds.; Fourth International Conference on Integrated Formal Methods (IFM 2004), 4–7 April 2004, Canterbury, GB, Springer, Berlin/Heidelberg, pp. 1–20 It probably stood for "Software, Languages, Analysis, and Modeling." Note that Microsoft has since re-used SLAM to stand for "Social Location Annotation Mobile".
See also
- Abstraction model checkingAbstraction model checkingAbstraction Model checking is for systems where an actual representation is too complex in developing the model alone. So, the design undergoes a kind of translation to scaled down "abstract" version....
- the BLAST model checkerBLAST model checkerThe Berkeley Lazy Abstraction Software Verification Tool is a software model checking tool for C programs. The task addressed by BLAST is the need to check whether software satisfies the behavioral requirements of its associated interfaces...
, a model checker similar to SLAM that uses "lazy abstraction"