SLAM project

The SLAM project, which was started in 1999 by 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."[1] It initially stood for "software (specifications), programming languages, abstraction, and model checking".[2] Note that Microsoft has since re-used SLAM to stand for "Social Location Annotation Mobile".[3]

See also

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

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. ^ Ball, Thomas; Levin, Vladimir; and Rajamani, Sriram K.; A decade of software model checking with SLAM; Communications of the ACM, Vol. 54(7), pp. 68–76 (July 2011)
  3. ^ Mondok, Matt; Microsoft's Slam: stay in touch with, stalk your friends; Ars Technica, 2006 October 10

External links

  • Official website
  • v
  • t
  • e
ML programming
Software
Implementations,
dialects
  • Caml
    • OCaml°
      • Eff
      • F*°
      • F#°
      • JoCaml°
      • Reason°
  • Concurrent ML
  • Dependent ML
    • ATS°
  • Futhark°
  • Lazy ML
  • MacroML
  • ML
  • Ur°
Programming tools
Theorem provers,
proof assistants
Community
Designers
  • Lennart Augustsson (Lazy ML)
  • Damien Doligez (OCaml)
  • Gérard Huet (Caml)
  • Xavier Leroy (Caml, OCaml)
  • Robin Milner (ML)
  • Don Sannella (Extended ML)
  • Don Syme (F#)
  • Italics = discontinued
  • ° = Open-source software
    Book Category:Family:ML Category:Family:OCaml Category:Software:OCaml
    • v
    • t
    • e
    Main
    projects
    Languages, compilers
    Distributed–grid computing
    Internet, networking
    Other projects
    Operating systems
    • Barrelfish
    • HomeOS
    • Midori
    • Singularity
    • Verve
    APIs
    Launched as products
    MSR Labs
    applied
    research
    Live Labs
    Current
    Discontinued
    FUSE Labs
    Other labs
    Category
    Stub icon

    This computer-engineering-related article is a stub. You can help Wikipedia by expanding it.

    • v
    • t
    • e