読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

第3回 Formal Methods勉強会に行ってきました。

FM-Forum 形式手法

第3回FormalMethods勉強会 : ATND
(via fm-forum @ ウィキ - トップページ)
場所は喫茶ルノアールというところの中にある会議室でした。
前半Alloyの話をid:kencobaさんが、後半はCoqの話をtmiyaさんがするという形式でした。13時から19時まで6時間でしたが興味深い話題がいろいろでて、あっという間という感じでした。

特に私が興味深いと感じたことは

  • 国際規格のISO/ICE 15408 や ISO/ICE 61508 などの情報技術セキュリティ評価基準の内容にformal method(形式手法)という言葉が明記された
  • Alloy検証機はシステム開発の上流工程で便利
  • Coq の WHYツールは自動検証もラクラクできる
  • 並列計算処理で検証を使った高信頼な開発ができたら注目されるかもしれない
  • Alloy本の和訳プロジェクト進行中
  • 形式手法は名古屋が熱い (自動車産業、組み込み系が活発だから)

懇親会のときにも感じましたが、高信頼なシステム開発のために より進んだ手法として形式手法に注目している方が多いように思いました。そういう意味ではCoqも形式手法の一つのツールとして特に実装面において非常に役に立つので効果的に使いたいですね。

懇親会後、3次会で一風変わった喫茶店(バー?)に行きましたが、そこでもPropとboolの違いなどについて熱く議論できて、最後まで非常に充実した時間を過ごすことができました。しかし、帰るためのバスがわからず、ご迷惑をかけてしまいました。一緒にバスを探してくださった tmiyaさん、mizoguchiさん、yshigeruさん ありがとうございました。