ある種のプログラム解析はモデル検査であるとの洞察に基づき、SMV を用いて Jimple プログラムを CTL-FV 論理式で検査する手法に関する論文。CTL-FV は変数を利用できるため状態が表現しやすく、プログラム解析の内容の記述が容易になる。SMV が受け付けるのは変数を含まない CTL 論理式なので、プログラム中の変数を CTL-FV 論理式中の変数に束縛する。変数束縛と Jimple プログラムの状態遷移モデルへの変換を同時に行い、SMV で検査する。

author="山岡 裕司 and 胡 振江 and 武市 正人 and 小川 瑞史",
title="{モデル検査技術を利用したプログラム解析器の生成ツール}",
journal="情報処理学会論文誌：プログラミング",
volumn="44",
number="SIG13(PRO18)",
pages="25--37",
year="2003"

コメント追加

投稿者 kw : 2008/08/06 10:29:24 JST #