静的コード解析の会第0回でVeriFastについて発表してきた - ::Eldesh a b = LEFT a

#静的コード解析の会第0回でC言語(とJava)の検証器であるVeriFastについて発表してきました。

資料は公開してあるので興味ある人は見てください。動画もあります。
> https://metasepi.connpass.com/event/42141/presentation/

結構(私の理解が)きわどい質問も出ましたが、大体伝えたかった内容は伝わったんじゃないかと思います。
個人的には手ぶらで(ぐだぐだ)発表したProofSummit2016のリベンジでもあったので資料はかなり頑張って作りました。(内容は全然違いますが

本当に詳しく知りたい人は公式チュートリアル読むべきなのですが、これは結構ヘビーな量と内容です。これに対して私の発表は「忙しい人向けの入門」といった感じなのでお気軽にどうぞ(^^)

他の発表について

CSPというのを初めて知りました。プロセス代数というのは(多分大学生の時に)聞いたことはあったんですが、通信するプリミティブがあるなぁ、くらいのことしか分かりませんでした。
今になって説明を聞くと、多少理論的な話や記号が出てもビビらなくなったし、なんとなく理解できる部分も増えていたので嬉しみがありました(なお、日本語力は低下したもよう…)
あとCMLに似てますね(これは多分関係が逆だけど)。

自分がここ数年多少なりとも理論的な話として勉強してきた内容は、主に(型付き)ラムダ計算とその意味論だったので、実装でも仕様でもない(あるいはどちらにもなる？)ものと意味論を扱うというのは新鮮でした。

他には具体的に気になったものとしてトレース意味論というのが紹介されていました。これはプログラムの副作用を形式的に扱う方面でも出てきてよく分からなかったんですが、CSPでの扱いはかなり明快だなという感じを受けました。(プロセス間の作用が初めから限定されているから当たり前か？
あとは「coinductive」という単語も出ていたので、それを持ち出す気持ちくらいは知りたいなという感じです。

気になるワードは他にも幾つか出ていたので忘れないうちにフォローしておきたいですね。

最後にInferですが、やはり残念だという結論のようです…。
個人的には少なくともFalse Positiveは出てほしくないですねぇ。
ヒューリスティクスでなく理論的基礎がしっかりしているということに期待出来る/したいのはそこだと思うので。