|
量的情報流の困難性に関する研究を行い、beliefやmin entropy channel capacityなど様々な情報理論的尺度に基づく量的情報流に関する検証・推論問題の困難性を解明した。計算量理論的困難性のみならず、「hyperproperty」と呼ばれるプログラム検証問題の分類を用いての困難性も考察した。また、ソフトウェアモデル検査技術と#SATソルバ等カウンティングアルゴリズムを応用した高精度な量的情報流上限検証・推論アルゴリズムを提案した。また、検証アルゴリズムの基礎となるソフトウェアモデル検査技術の改良に関する研究を行った。
|
