@article{oai:kutarr.kochi-tech.ac.jp:00000123,
 author = {新田, 直也 and 高田, 喜朗 and 関, 浩之},
 issue = {4},
 journal = {電子情報通信学会論文誌. D, 情報・システム = The IEICE transactions on information and systems},
 month = {Apr},
 note = {Java development kit 1.2のように，プログラム実行時に制御スタックを検査することでアクセス制御を行うようなプログラム環境がある．Jensenらは，プログラム P 及び時相論理式を用いて記述された検証条件 ψ を与えたときに，P の到達可能な状態すべてが ψ を満たすかどうかを決定する問題として検証問題を定義し，相互再帰を含まないプログラムのクラスに対して検証問題が決定可能となることを示した． 本論文では，時相論理式よりも真に表現能力の大きい正規言語を用いて検証問題を定義する．そして，プログラムのトレース集合がインデックス言語となることを示し，その系としてプログラムが相互再帰を含む場合も含めて検証問題が一般に決定可能となることを示すことにより，Jensenらの結果を改善する．更に，自明なスタック検査のみを含むプログラムのクラスに対する検証問題が，プログラムサイズに対して多項式時間可解であることを示す．},
 pages = {360--370},
 title = {スタック検査機能をもつプログラムに対するセキュリティ検証問題の決定可能性},
 volume = {J85-D1},
 year = {2002}
}