「簡明な仕様記述法とそれを使ったソフトウェア開発支援について研究しています」

パソコンのソフトだけでなく、携帯電話器から人工衛星、発電所など、世の中のさまざまなものがソフトウェアで制御されています。 一見正しい動作をしているようでも、偶然が重なったときに突如不具合を起こしたり停止したりする、というのでは困りますが、このような誤り(バグ)を完全になくすのは非常に難しことです。 ソフトウェアが正しく動作するということを、厳密に、理詰めで確かめる方法や、そのような検証がしやすい仕様記述方法について研究しています。