ある種のプログラム解析はモデル検査であるとの洞察に基づき、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 #

プログラム中で生成される文字列を文脈自由文法で近似して、正規表現による仕様との disjoint を検査する話。PHP を対象として実装して、XSS や生成される HTML の妥当性が検査できる。

author="Yasuhiko Minamide",
title="{Static Approximation of Dynamically Generated Web Pages}",
booktitle="Proc. of the 14th International World Wide Web Conference",
publisher="ACM Press",
pages="432--441",
year="2005"

コメント追加

投稿者 kw : 2008/08/01 10:43:31 JST #