SLAMプロジェクト

SLAMプロジェクトは、1999 年にMicrosoft Researchの Thomas Ball と Sriram Rajamani によって開始され、モデル検査技術を使用してソフトウェアの安全性プロパティを検証することを目的としていました。OCaml で実装され、 Windows デバイスドライバーの多くのバグを見つけるために使用されました。Microsoft Windows Driver Foundation開発キットの一部として、Static Driver Verifier (SDV) として配布されています。「SLAM は元々頭字語でしたが、説明するのが面倒すぎると感じました。現在は、プログラム内のバグを「スラム」すると考えることを好みます。」^[1]当初は「ソフトウェア (仕様)、プログラミング言語、抽象化、およびモデル検査」の略でした。^[2] Microsoft はその後、SLAM を「Social Location Annotation Mobile」の略語として再利用していることに留意してください。^[3]

参照

抽象化モデルチェック
BLASTモデルチェッカーは、SLAMに似た「遅延抽象化」を使用するモデルチェッカーです。

参考文献

^ Ball, Thomas; Cook, Byron; Levin, Vladimir; および Rajamani, Sriram K.; SLAM および Static Driver Verifier: Microsoft 社内における形式手法の技術移転; Lecture Notes in Computer Science (LNCS)、第 2999 巻: Boiten, Eerke A.; Derrick, John; および Smith, Graeme; 編; Fourth International Conference on Integrated Formal Methods (IFM 2004)、2004 年 4 月 4 ～ 7 日、カンタベリー、GB、Springer、ベルリン/ハイデルベルク、pp. 1 ～ 20
^ Ball, Thomas; Levin, Vladimir; Rajamani, Sriram K.; SLAM によるソフトウェアモデル検査の 10 年間; Communications of the ACM, Vol. 54(7), pp. 68–76 (2011 年 7 月)
^ モンドック、マット、マイクロソフトのスラム：友達と連絡を取り合い、ストーカー行為をする、Ars Technica、2006年10月10日

外部リンク

公式サイト

[1] Ball, Thomas; Cook, Byron; Levin, Vladimir; および Rajamani, Sriram K.; SLAM および Static Driver Verifier: Microsoft 社内における形式手法の技術移転; Lecture Notes in Computer Science (LNCS)、第 2999 巻: Boiten, Eerke A.; Derrick, John; および Smith, Graeme; 編; Fourth International Conference on Integrated Formal Methods (IFM 2004)、2004 年 4 月 4 ～ 7 日、カンタベリー、GB、Springer、ベルリン/ハイデルベルク、pp. 1 ～ 20

[2] Ball, Thomas; Levin, Vladimir; Rajamani, Sriram K.; SLAM によるソフトウェアモデル検査の 10 年間; Communications of the ACM, Vol. 54(7), pp. 68–76 (2011 年 7 月)

[3] モンドック、マット、マイクロソフトのスラム：友達と連絡を取り合い、ストーカー行為をする、Ars Technica、2006年10月10日