プログラミングの面倒を倒すための研究

現代社会を支える膨大なプログラム。私たちはそれらが、正しく動くと思いがちですが、実際には常にバグ（処理の遅延や誤作動）や情報漏洩のリスクが潜んでいます。
本研究室では、プログラムを数学的に解析し、その正しさや効率を理論的に保証する基盤技術を研究しています。単に動くだけではない、本当に「良いプログラム」をどう設計するか。ソフトウェアの信頼性を根底から支え、社会の安心を、より確かなものへと進化させます。