静的コード解析の会#6で発表してきた
静的コード解析の会#6でVeriFastによる停止性検査について発表してきました。(資料作って徹夜してしまった…)
前回も同じテーマでしたが私の理解も資料も十分でなかったため(α)としてました。
が、今回の発表では多重集合、整礎関係、実際の処理系で検査できるコードについての説明まで入れることが出来たので、これで一通りの内容を盛り込めたと思います(ただしシーケンシャルなプログラムに限る…)。
参照している論文はModular termination verificationです。
(多分)怪しげな記述や展開のよく分からないページがありますが、がんばって作ったので興味がある人は是非眺めてみて下さい。
個人的なおすすめはStatic Recursionパターンの検証方法のあたり(資料の末尾の方)です。
会場からは、
- 処理系が(もっと)がんばれ
- 発表の構成が悪い(直接そうは言われてないけど)
という感じの反応が得られました…orz。
感想
これまで何度かVeriFastに関する発表をしてるし、(呑みながら)議論もしてきたので聴衆の理解度が高くて非常に楽しい発表になりました。ありがとうございました。
また、懇親会でマルチスレッドの扱いについて質問がありました。通常の(部分正当性の)検査では問題無くスレッドが扱えますが、停止性検査については全く把握できていないので基本的なアイディアだけでも押さえておきたいと思っています。
参照した論文のTR版にマルチスレッドに関する議論があるようです。
