文献

J-GLOBAL ID：201002238439757476   整理番号：10A1461849

特性形式を通じたプログラム検証

Program Verification Through Characteristic Formulae

著者 (1件)： CHARGUERAUD Arthur (INRIA)
資料名： ACM SIGPLAN Notices (Association for Computing Machinery. Special Interest Group on Programming Languages)  (ACM SIGPLAN Notices (Association for Computing Machinery. Special Interest Group on Programming Languages))
巻： 45  号： 9  ページ： 321-332  発行年： 2010年09月 
JST資料番号： D0915A  ISSN： 0362-1340  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 既存の純関数プログラムOCamlのソースコードを,形式的に特定・検証する効果的技法CFML(特性形式に基づく検証ツール)について記述した。Hondaなどのtotal characteristic assertion pairsを改良した特性形式は,ソースから各トップレベル定義に関する論理式を体系的に生成し,標準高階論理結合による表現がプログラム動作を正確に説明する。その後,Coqなどの証明アシスタントを利用した特性形式の推論により,プログラム検証を行う。OCamlのパーサと型検査器を再利用して最大の互換性を確保し,既存コードの検証を可能にした。提案ツールを多数の純関数型データ構造に適用し,高階論理による複雑な不変量の簡潔表現,インタラクティブ証明による証明義務からの容易な解放,比較的迅速な検証プロセスなどを示した。

シソーラス用語： *プログラム検証 ,  *関数プログラミング ,  *形式的手法【計算機】 ,  式 ,  高階論理 ,  プログラム理解 ,  データ構造 ,  構文分析 ,  不変量 ,  仕様記述 ,  正規化 ,  埋込み【挿入】
準シソーラス用語： 論理式

分類 (1件)： 計算機システム開発  (JD02010R)

タイトルに関連する用語 (2件)： 形式 ,  プログラム検証