文献

J-GLOBAL ID：201202200080970869   整理番号：12A1689840

高階モデル検査用の走査ベースアルゴリズム

A Traversal-based Algorithm for Higher-Order Model Checking

著者 (3件)： NEATHERWAY Robin P. (Univ. Oxford) ,  ONG C.-H. Luke (Univ. Oxford) ,  RAMSAY Steven J. (Univ. Oxford)
資料名： 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))
巻： 47  号： 9  ページ： 353-364  発行年： 2012年09月 
JST資料番号： D0915A  ISSN： 0362-1340  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 過去10年に渡って,モデル検査が多大な努力を有してプログラム検証に対して適用されて来た。本論文において,筆者らは決定論的自明オートマトンに対するcaseを有した高階再帰方式(HORSC)用の普遍モデル検査問題に対する実用的アルゴリズムを提示した。本アルゴリズムは走査に基づいており,再帰方式の完全抽象ゲーム意味論によって誘因された。筆者らはHORSCモデル検査を抽象-詳細化手続きを介して関数型言語(パターンマッチング再帰方式として提示される)を検証するためのアプローチに対する適切なバックエンドと見做している。筆者らのツール実装を用いた予備実験は,本アルゴリズムが数百の規則を有した方式を生成する小さいが現実的な数多くの例上で驚くほど良く機能する事を示した。

シソーラス用語： *モデル検査 ,  高階論理 ,  関数型言語 ,  *走査 ,  再帰性 ,  プログラム検証 ,  プッシュダウンオートマトン ,  抽象 ,  ゲーム ,  意味論 ,  *アルゴリズム

分類 (4件)： 計算機システム開発  (JD02010R) ,  応用プログラミング言語  (JD03052Y) ,  論理代数  (JB03000H) ,  オートマトン理論  (JB04000O)

タイトルに関連する用語 (3件)： モデル検査 ,  走査 ,  アルゴリズム