大規模プログラムのためのプログラム解析の自動生成

点击翻译按钮获取中文摘要

近年、モデル検査の実装技術の発達とハードウェアの進歩により、「プログラム解析=抽象化+モデル検査」というパラダイムが現実的なものとなっている。たとえば、既存のモデル検査系SMVを、Javaを中間言語Jimpleへ変換する言語処理環境SOOTと組み合わせることで、簡単にプログラム解析を実装することが可能である。これは小〜中規模のプログラムに対して有効であるが、処理時間がサイズとともに急速に増大し、大規模プログラムの解析をどう行うかは、現在ホットな研究領域である。この処理時間増大の原因の一つは、モデル検査などで標準的なアルゴリズムが収束するまで何度も反復してプログラム全体を追跡するためである。本研究では、実際のプログラムのフローグラフは比較的良い構造をもっているという観察に基づき、モデル検査のアルゴリズムから見直しをはかることで、大規模なプログラムへの適用可能性を探ることを提案した。具体的には、(1)組み合わせ理論の成果を用いて、すでに提案してきたグラフの代数的データ構造(SP項)に基づき、反復がなく効率の良いアルゴリズムおよびその理論的基礎の確立、(2)実用的な問題におけるケーススタディによる問題点の明確化について研究を行った。