El proyecto SLAM , que fue iniciado en 1999 por Thomas Ball y Sriram Rajamani de Microsoft Research , tenía como objetivo verificar las propiedades de seguridad del software utilizando técnicas de verificación de modelos . Se implementó en OCaml y se ha utilizado para encontrar muchos errores en los controladores de dispositivos de Windows. Se distribuye como parte del kit de desarrollo de Microsoft Windows Driver Foundation como Static Driver Verifier (SDV). "SLAM originalmente era un acrónimo, pero nos resultó demasiado engorroso explicarlo. Ahora preferimos pensar en 'bloquear' los errores en un programa". [1] Probablemente significaba "Software, lenguajes, análisis y modelado". [2]Tenga en cuenta que, desde entonces, Microsoft ha reutilizado SLAM para representar "Social Location Annotation Mobile". [3]
Ver también
- Comprobación del modelo de abstracción
- el verificador de modelos BLAST , un verificador de modelos similar a SLAM que utiliza "abstracción perezosa"
Referencias
- ^ Bola, Thomas; Cook, Byron; Levin, Vladimir; y Rajamani, Sriram K .; SLAM and Static Driver Verifier: Transferencia de tecnología de métodos formales dentro de Microsoft ; Lecture Notes in Computer Science (LNCS), vol. 2999: Boiten, Eerke A .; Derrick, John; y Smith, Graeme; eds .; Cuarta Conferencia Internacional sobre Métodos Formales Integrados (IFM 2004), 4 a 7 de abril de 2004, Canterbury, GB , Springer, Berlín / Heidelberg, págs. 1 a 20
- ^ Central de desarrolladores de hardware de Microsoft Windows; Glosario de siglas para PC y tecnologías de servidor ; 2007 26 de febrero
- ^ Mondok, Matt; Microsoft's Slam: mantente en contacto, acecha a tus amigos ; Ars Technica, 10 de octubre de 2006