Clarke 先生の講演＠計算機言語談話会
大阪の千里にある産業技術総合研究所のシステム検証研究センターでは、隔週くらいの頻度で計算機言語談話会というものが開かれています。モデル検査や対話型定理証明の講演を無料で聞くことができるというありがたいイベントですが、平日の昼間に開催という壁に阻まれ、いままで参加できずにいました。ですが、今回はモデル検査研究の第一人者であり、Model Checking の著者でもある CMU の Ed Clarke 博士の講演があるということで午後半休を取って受講してきました。
講演の内容は、モデル検査の生誕から25年の道のりをざっくり解説しつつ、ハードウェアからソフトウェアへと適用範囲を広げてきたモデル検査が、ソフトウェアモデル検証の研究で培われてきたテクニックを生かして、またハードウェアの検証に戻ってきた、というようなお話でした。ハードウェアは最近 VHDL などの高水準な形式で記述されることが多くなりましたので、そのレベルで検証をかけると効果的であるということのようです。強調していたのは、ハードウェアには再帰もポインタもヒープからのメモリ確保もない、ということ*1。裏返せば、そういったものの扱いがとても困難で、ソフトウェアのモデル検査に関してはある種の壁にぶつかっているということでもあるのかもしれませんね*2。
ちなみに、ゲームのスクリプト言語は同様にポインタやヒープがないことが多いですので、実はモデル検査に非常に向いている応用です。モデル検査を使えば、複雑に絡み合ったシナリオ遷移と大量のフラグ群に対して、自動的に全数探索（に理論的に相当する作業）をかけて、到達できないパートがないことやハマり状態が存在しないことなどを保証することが可能になります。興味がある方はぜひ調べてみてください。というか、それが僕の修士論文だったわけですが……。関連論文はこちら。
しかし、講演が終わったあとの雑談で、BDD (Binary Decision Diagram) は 1980 年代の技術だと思っている、と言われてしょんぼりしてしまいました。学生時分に SAT Solver を利用した Bounded Model Checking はハードウェアの検証にしか使えないなぁ、と判断した記憶があるのですが,
どうもそれは僕の勘違いだったようで。今やモデル検査といえば SAT Solver という感じになっている雰囲気でした。いい論文があるからあとで紹介するよ、と言っていただけたので、勉強しないと……。
ちなみに、Model Checking にはまだ BDD しか載っていないのですが、SAT Solver の利用についても記述した第二版が出版されるとのことです。出たら買わないと……。というか、和訳してくださる出版社はいないものでしょうか（涙）
本といえば、産総研のシステム検証研究センターから日本語のモデル検査の本が出版されたようです！Amazon でも買えます: 「4日で学ぶモデル検査 (初級編) (CVS教程 (1))」学生時代に日本語の文献がまったくなくて困ったことを考えると、よい時代になったものです……。
講演の後、教授と奥様と一緒に夕食をとりませんか、という話がありましたので、ちゃっかりと混ぜてもらってきました。魚と根菜類を中心としたおいしい懐石料理に舌鼓を打ちつつ、正体不明の食材を英語で表現する方法に頭を悩ませながら、楽しい時間をすごさせていただきました。しかし、Clarke 先生はこの来日で日本を縦断しつつ7回も講演されるとのこと。人気者はたいへんですね……。
