SLAM project

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."[1] It probably stood for "Software, Languages, Analysis, and Modeling."[2] Note that Microsoft has since re-used SLAM to stand for "Social Location Annotation Mobile".[3]

See also

References

  1. ↑ Ball, Thomas; Cook, Byron; Levin, Vladimir; and Rajamani, Sriram K.; 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
  2. ↑ Microsoft Windows Hardware Developer Central; Glossary of Acronyms for PC and Server Technologies; 2007 February 26
  3. ↑ Mondok, Matt; Microsoft's Slam: stay in touch with, stalk your friends; Ars Technica, 2006 October 10

External links

This article is issued from Wikipedia - version of the Wednesday, July 15, 2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.