プログラム定理証明

弊社での、プログラム定理証明を用いたソフトウェア品質保証の取り組みについて紹介します。

iZE Smart Desktopミドルウェアの正しさ検証

(ソフトウェア科学会PPL2010においてポスター発表、TPP10にて発表)

(有)ITプランニングは(株)アイズの「スマートデスクトップ・クライアント」の一部モジュールを請負開発し，その際証明支援器Coqを使用した． 本プロジェクトではD-Busで扱うデータとJSONとの相互変換に関して静的検証を行った． 具体的には，検証対象とする関数をCoqで定義した上で諸性質を証明し，Extract機能により全体のOCamlのプログラムと協調させるという方法を用いた． 今回行った検証の詳細と，実際にCoqを開発現場で使う上で行った工夫などを報告する． (PPL2010予稿集より)

スライドをダウンロード(PDF,英文)

プログラム定理証明って？

プログラム定理証明は、プログラムの正しさを検証する形式手法の一つです。 プログラム定理証明は、Coq、Agdaなどの定理証明支援系と呼ばれるツールを用いて行うことが多いです。

  • QCon Tokyo 2011(2011/4/12)で弊社今井宜洋がプログラム定理証明の応用について講演致します！
  • ProofCafeは、プログラム定理証明に興味がある国内の技術者が名古屋に集まる勉強会です。 これまでに Coq庵、Coq Partyなどのイベントが企画されました。