| 研究実績の概要 |
メモリ一貫性モデルを考慮したモデル検査における状態爆発問題に対し、リオーダリングされる命令の制御という解決手法の提案を行い、それを開発しているモデル検査器 McSPIN に実装し、評価を行った。それらに関して執筆した論文は、国際会議 9th Working Conference on Verified Software: Theories, Tools, and Experiments に採択された。Garbage Collection の代表的な教科書である Jones et al.「The Garbage Collection Handbook」に載っている並行 GC を McSPIN で検査し、知られていないバグ 2 つを発見し、それに関する論文が国際会議 The 32nd OOPSLA に採択された。平成28年度に構築したプログラム論理においてもプログラムの表現として利用されている directed acyclic graph を検査するモデル検査器 VeriDAG を開発し、これに関する論文が The 13th Haifa Verification Conference に採択された。メモリ一貫性モデルを考慮したモデル検査器 SPIN 用のライブラリに関する、共同研究をしている松元稿如氏・鵜川始陽博士との共著論文が Journal of Information Processing に採択された。
|
