Proyecto SLAM

El proyecto SLAM , iniciado en 1999 por Thomas Ball y Sriram Rajamani de Microsoft Research , tenía como objetivo verificar las propiedades de seguridad del software mediante técnicas de comprobación de modelos . Se implementó en OCaml y se ha utilizado para encontrar numerosos errores en los controladores de dispositivos de Windows. Se distribuye como parte del kit de desarrollo de Microsoft Windows Driver Foundation como el Verificador Estático de Controladores (SDV). "SLAM era originalmente un acrónimo, pero nos pareció demasiado engorroso de explicar. Ahora preferimos pensar en 'golpear' los errores en un programa". ^{[ 1 ]} Inicialmente significaba "software (especificaciones), lenguajes de programación, abstracción y comprobación de modelos". ^{[ 2 ]} Desde entonces, Microsoft ha reutilizado el acrónimo SLAM para significar "Social Location Annotation Mobile" (Anotación de Ubicación Social Móvil). ^{[ 3 ]}

Véase también

Verificación de modelos de abstracción
el verificador de modelos BLAST , un verificador de modelos similar a SLAM que utiliza "abstracción perezosa".

Referencias

↑ Ball, Thomas; Cook, Byron; Levin, Vladimir; y Rajamani, Sriram K.; SLAM y 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-7 de abril de 2004, Canterbury, GB , Springer, Berlín/Heidelberg, pp. 1-20
↑ Ball, Thomas; Levin, Vladimir; y Rajamani, Sriram K.; Una década de verificación de modelos de software con SLAM ; Communications of the ACM, Vol. 54(7), pp. 68–76 (julio de 2011)
↑ Mondok, Matt; Slam de Microsoft: mantente en contacto con tus amigos, acosa a tus amigos ; Ars Technica, 10 de octubre de 2006

Enlaces externos

Sitio web oficial

[1] Ball, Thomas; Cook, Byron; Levin, Vladimir; y Rajamani, Sriram K.; SLAM y 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-7 de abril de 2004, Canterbury, GB , Springer, Berlín/Heidelberg, pp. 1-20

[2] Ball, Thomas; Levin, Vladimir; y Rajamani, Sriram K.; Una década de verificación de modelos de software con SLAM ; Communications of the ACM, Vol. 54(7), pp. 68–76 (julio de 2011)

[3] Mondok, Matt; Slam de Microsoft: mantente en contacto con tus amigos, acosa a tus amigos ; Ars Technica, 10 de octubre de 2006

[ 1 ]

[ 2 ]

[ 3 ]