文献

J-GLOBAL ID：200902219840947533   整理番号：09A0289510

フロー準拠プログラムマッチングの基礎 時相論理とモデル検査の使用

A Foundation for Flow-Based Program Matching: Using Temporal Logic and Model Checking

著者 (5件)： BRUNE Julien (Univ. Copenhagen, DNK) ,  DOLIAEZ Damien (INRIA, FRA) ,  HANSEN Rene Rydhof (Aalborg Univ., DNK) ,  LAWALL Julia L. (Univ. Copenhagen, DNK) ,  MULLER Gilles (Ecole des Mines de Nante, FRA)
資料名： 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))
巻： 44  号： 1  ページ： 114-126  発行年： 2009年01月 
JST資料番号： D0915A  ISSN： 0362-1340  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： プログラムに制御フローパスに関する推論は,最近のプログラムマッチング言語や,これに関連する探索,変換ツールの重要機能である。時相論理は制御フローパスの特性を表現する有力な手段を提供し,時相論理を拡張したCTL(計算ツリー論理)は最適化コンパイラが通常実行するプログラム変換の記述と検証に適用されている。しかしLinuxのコラテラル進化実行のために筆者らが開発した,Coccinelleプログラム変換ツールの開発には,既存のCTLツールは不十分であった。本論文では,Coccinelleプログラムマッチング言語の意味論と実装に適した,CTLを拡張したCTL-VW(自由変数を伴うCTL)を提案した。この拡張は,プログラム断片にわたる存在的限量化を含み,これによりプログラムマッチング言語中のメタ変数が,制御フローパス内の異なる値にわたることができる。CTL-VWを形式化し,そのCoccinelleにおける使用を述べた。Linuxコード中のバグ修正事例により,この手法の性能を評価した。

シソーラス用語： 計算機プログラム ,  マッチング ,  *時間論理 ,  モデル検査 ,  プログラム解析 ,  プログラム変換 ,  仕様記述 ,  コンパイラ ,  Linux ,  *意味論 ,  応用向き言語 ,  形式的手法【計算機】 ,  デバッギング ,  計算機アルゴリズム ,  健全性 ,  性能評価 ,  記号論理 ,  変数 ,  制御フロー解析

分類 (2件)： 計算機システム開発  (JD02010R) ,  応用プログラミング言語  (JD03052Y)

タイトルに関連する用語 (5件)： フロー ,  マッチング ,  基礎 ,  時相論理 ,  モデル検査