Static Driver Verifier

すごい。。。こんなツールが。
http://news.goo.ne.jp/news/wired/it/20051116/20051116304.html

SDVは「モデル検査」という手法を使い、ウィンドウズ用デバイスドライバーのソースコードを分析して、ドライバーが本来行なうべきことを数学的にモデル化したものと、プログラマーが書いたコードが一致するかどうかを調べる。ドライバーがモデルと一致しない場合、SDVがドライバーにバグがあるかもしれないと警告する。

つーか、これ公開したらドライバの精度が飛躍的に向上する可能性もあるよな。
モデルプログラミングの時代といわれて久しいが、これで低層のプログラマが要らなくなるとしたら、ある意味恐ろしい時代が来たとも言えるかも。