View source for SLAM project

{{Short description|Microsoft research project}}
The '''SLAM project''', which was started in 1999 by [[Thomas Ball (computer scientist)|Thomas Ball]] and [[Sriram Rajamani]] of [[Microsoft Research]], aimed at verifying software safety properties using [[model checking]] techniques. It was 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 originally was an acronym but we found it too cumbersome to explain. We now prefer to think of 'slamming' the bugs in a program."<ref >Ball, Thomas; Cook, Byron; Levin, Vladimir; and Rajamani, Sriram K.; [http://research.microsoft.com/pubs/70038/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</ref> It initially stood for "software (specifications), programming languages, abstraction, and model checking".<ref>Ball, Thomas; Levin, Vladimir; and Rajamani, Sriram K.; [https://doi.org/10.1145/1965724.1965743 ''A decade of software model checking with SLAM'']; Communications of the ACM, Vol. 54(7), pp. 68–76 (July 2011)</ref> Note that Microsoft has since re-used SLAM to stand for "Social Location Annotation Mobile".<ref>Mondok, Matt; [https://arstechnica.com/microsoft/news/2006/10/5573.ars ''Microsoft's Slam: stay in touch with, stalk your friends'']; Ars Technica, 2006 October 10</ref>

==See also==
* [[Abstraction model checking]]
* the [[BLAST model checker]], a model checker similar to SLAM that uses "lazy abstraction"

==References==
{{Reflist}}

==External links==
*{{Official website|research.microsoft.com/slam}}

{{ML programming}}
{{Microsoft Research}}

[[Category:Formal methods]]
[[Category:OCaml software]]
[[Category:Microsoft Research]]

{{Comp-eng-stub}}