<< Typestate: A Programming Language Concept for Enhancing Software Reliability | ホーム | 動的解析によるWebアプリケーション・モデル抽出支援手法 >>

Combining Type-Based Analysis and Model Checking for Finding Counterexamples Against Non-Interference

情報流解析のための型システムで型が付かなかったプログラムが本当に危ないのかモデル検査によって確認するという論文。検査すべきパスを見つけたり枝刈りしたりアルゴリズムがちゃんと提案されていて、C 言語のサブセットに対して実験している。

author="Hiroshi Unno and Naoki Kobayashi and Akinori Yonezawa",
title="{Combining Type-Based Analysis and Model Checking for Finding Counterexamples Against Non-Interference}",
booktitle="PLAS'06",
publisher="ACM",
pages="17--26",
year="2006"

http://dx.doi.org/10.1145/1134744.1134750

タグ : ,
コメント追加 RSS feed for responses to this blog entry
投稿者 kw : 2008/09/12 16:53:11 JST #



コメント追加 トラックバック送信