プログラムの正しさを数学的に証明する形式検証への招待
Twitter眺めてたら面白そうなセミナーがあったので申し込んだ。
私はオブジェクトストレージではないPOSIX IFな分散ファイルシステムを作るという面白い仕事をもう数年間ぐらい続けている。
その関係で最近TLA+とTLC Model Checkerを業務で使っている。私が「導入すべき」と宣言して先陣を切った感じ。そのため、形式仕様記述言語やTheorem ProvingやModel checkerへの興味がぐんと増している。せっかくなのでいろいろ教えてもらおう。
定理証明支援系はCoqというものがあるということぐらいしか知らないし、そもそもCoqが何を手伝ってくれるのかすらよく理解してないのでいい機会だと思う。
このセミナーではIsabelleというものを使うそうだが。これは初耳。楽しみ。
