東京理科大学学士（応用数学）（1994），北陸先端科学技術大学院大学修士(情報科学)（1996），北陸先端科学技術大学院大学博士(情報科学)（1999）
2016 - : 北陸先端科学技術大学院大学 , 先端科学技術研究科 , 教授
2009 - 2016 : 北陸先端科学技術大学院大学 , 情報科学研究科 , 助教授
2006 - 2009 : 北陸先端科学技術大学院大学 , 安心電子社会研究センター , 特任助教授
2001 - 2005 : 科学技術振興事業団 , さきがけ研究２１「機能と構成」領域 , 研究員
1999 - 2006 : 北陸先端科学技術大学院大学 , 情報科学研究科 , 助手
ソフトウェア
形式手法, 形式検証, 車載システム, ソフトウェアテスト, ソフトウェア工学, モデル検査, 定理証明, 形式仕様
ソフトウェアの原理
プログラム意味論やプロセス代数といったソフトウェアに関連する基礎理論が古く
から研究され続けており，成熟しつつある．このような基礎理論を用いて，現在の
ソフトウェアの原理を明らかにすることは，今後のソフトウェアの健全な発展のた
めに重要である．そこで，現在，なんとなくソフトウェア開発で用いている記法や
概念を，プログラム意味論などの枠組を用いて形式化して，その原理を明らかする
研究を行っている．
形式手法/形式検証
形式手法では，数学を基礎とした言語やルールを用いて，対象となるソフトウェア
を記述し検証する．これにより，なんとなくソフトウェアを開発するのではなく，
数学にも基づいた解析や正しさの保証を行うことができる．また，ソフトウェアの
正しさを保証する１つの手法として，厳密に記述して正しいことを証明する方法が
考えられる．この方法のことは形式検証(Formal Verification)と呼ばれている．
そこで，このような形式手法／検証手法を用いて正しいソフトウェアを効率的に開
発する手法について研究を行っている．また，その適用対象として，主に，オブジェ
クト指向分析・設計法，組み込みソフトウェア開発に焦点を当てている．
ACM, IEEE, 情報処理学会, 電子情報通信学会, 日本ソフトウェア科学会
International Workshop on Software Technologies for Future Dependable Distributed Systems , Workshop Co-Chair , 2009 , Waseda University
SPLC 2007 Doctoral Symposium , Symposium co-chair , 2007
情報処理学会 組込みシステムシンポジウム , プログラム委員長 , 2006 - 2006
・ 14th International Symposium on Theoretical Aspects of Software Engineering , PC chair 2020
・ 14th International Conference on Formal Engineering Methods , Program Co-Chair 2012 - 2012
・ Best Paper Award , Mengwei Xu, Peter Riviere, Toshiaki Aoki, Marie Farrell, Yamine Ait-Ameur, Neeraj Singh, Guillaume Dupon , 12th International Conference on Rigorous State Based Methods(ABZ) , 2026
・ FOSS Award Runner-up , Yuki Takei, Toshiaki Aoki, Chaiyong Ragkhitwetsagu , Mining Software Repositories (MSR) 2026 , 2026
・ 第十二回善吾賞 , 青木利晃, 川上大介, 千田伸男, 冨田尭 , ソフトウェアテスト技術振興協会 , 2019