研究課題
最終年度には次の研究を実施した。１． 前年度・前々年度に行った研究を継続・発展し、また、将来的研究課題を開拓した(後述)。具体的には、時相論理仕様検証の研究、述語抽象・反例を用いた抽象詳細化などソフトウェアモデル検査の基盤技術の研究、また、オブジェクト指向言語に対する検証技術の研究を引き続き行った。２． プログラム検証技術の応用として、情報セキュリティ研究を行った。具体的には、サイドチャネル攻撃に対する耐タンパー性を持つプログラムの合成の研究と、プログラム検証によるタイミング攻撃の検出の研究を行った。成果をまとめた論文は、それぞれ、国際会議POST 2017とPLDI 2017に採録決定している。研究期間全体を通じて実施した研究を総括すると、時相論理仕様など型システムによる高階プログラムのためのソフトウェアモデル検査手法が扱える性質の拡張、また、ソフトウェアモデル検査など近代の高精度検証の基盤技術である述語抽象における抽象詳細化の改良、などが主な研究成果として挙げられる。これらの結果は、現実の大規模高階プログラムの高精度な検証の重要なファクターになると期待できる。しかし、現実の大規模ソフトウェアは（特に代数データ構造やオブジェクト等の再帰データ構造に対する）破壊的代入を含むものも多く、検証技術をそのようなプログラミング言語機能へ拡張する必要があるという事実も確認した。今後の研究の展開のための課題とする。例えば、分離論理(separation logic)やエイリアス型など、データ構造に対する破壊的代入を扱うためのプログラム論理・型システム等のアイデアを参考に効果的な検証技術を考える。
すべて 2017 2016
すべて 雑誌論文 (2件) (うち国際共著 2件、 査読あり 2件、 オープンアクセス 2件、 謝辞記載あり 2件) 学会発表 (1件) (うち招待講演 1件)
Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2017)
巻: 印刷中 ページ: 印刷中
-
Proceedings of the 6th International Conference on Principles of Security and Trust (POST 2017)
