無関係でもあるまい。もうすぐPLDI 2002で発表されるようだが、

> Flow-Sensitive Type Qualifiers
> Jeffrey S. Foster, Tachio Terauchi, Alex Aiken (University of California at Berkeley, USA)

なんかどうよ？　型システムに基づく静的検証で、Linuxカーネルのバグをいくつか見つけたらしいぞ。
ロックまわりとか。検索したらwebにも論文があったような。なんか定式化が微妙に変だったけど…
（Aikenがちゃんとチェックしなかったのか？）