文献

J-GLOBAL ID：201102266599447741   整理番号：11A1221911

高次モデル検査のための述語抽象とCEGAR

Predicate Abstraction and CEGAR for Higher-Order Model Checking

著者 (3件)： KOBAYASHI Naoki (Tohoku Univ.) ,  SATO Ryosuke (Tohoku Univ.) ,  UNNO Hiroshi (Tohoku Univ.)
資料名： 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))
巻： 46  号： 6  ページ： 222-233  発行年： 2011年06月 
JST資料番号： D0915A  ISSN： 0362-1340  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 近年,高次再帰スキームのモデル検査が関数型プログラムの検証に適用された。再帰スキームは無限ツリーを記述するための文法で,再帰スキームモデル検査は生成されたツリーが所与の特性を満足するかに関心がある。モデル検査は再帰性と有限データ領域を伴う,単純型付きλ計算で記述されたプログラムの特性を自動的に決定できる。整数などの無限データ領域を利用するプログラムの自動検証を実現すべく,述語抽象とCEGAR(counterexample-guided abstraction refinement)技法を提案し,プロトタイプ検証器の実装と複数のプログラムに対する試験を行った。提案方式は高次関数型プログラムの自動検証に有用であるが,実装の最適化,大規模な試験およびスケーラビリティが今後の課題である。

シソーラス用語： *モデル検査 ,  述語論理 ,  *抽象解釈 ,  再帰性 ,  ツリー構造 ,  λ計算 ,  *関数プログラミング ,  型推論 ,  Boole関数 ,  仕様記述 ,  データ型 ,  キャラクタリゼーション ,  型システム

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

タイトルに関連する用語 (3件)： モデル検査 ,  述語 ,  抽象