Research topics
実時間並行ソフトウェア開発手法
実世界で使用されているシステムの多くは，同時並行的に動作する複数のシステムの組み合わせで構成されています． 多くの場合，それぞれのシステムは「ある時間までに処理を完了しなければならない」といった時間的な制約を満たす必要があります． これらのシステムがCPUやメモリなどの資源を共有して動作するとき，正しく振る舞うかどうかを調べるのは難しい問題です．
結縁・中澤研究室では，”動作の正しさが保証されている” 実時間並行システムを “コストを抑えて” 開発する手法を研究しています． 主な研究分野は，プロセス代数や時間オートマトンなどの形式的手法の基礎理論， およびそれらの形式的手法に基づく開発手法 (モデル化，モデル検査，コード生成)などです。
プログラム解析・プログラム検証
プログラムはとにかく動けばよいというわけではありません． 「どんな入力を与えても必ず停止する」など，開発者の意図したとおりに振る舞うことが重要です． このような性質を満たすことを保証するためには，どうすればよいでしょうか． すべての入力についてテストすればよいと思うかもしれません． 入力のドメインが小さい場合はそれもよいでしょう． しかし，一般的には入力は無限にあり，すべてをチェックすることなど到底不可能です．
結縁・中澤研究室では，プログラムが特定の性質を満たすことを数理的な手法を用いて証明する研究を行なっています． 具体的には，モデル検査，抽象解釈，型システムなどについて研究しています． 証明と言っても，高校数学のように人間が頭を捻って考えるばかりではなく， コンピュータを使って自動化できることも多くあります． このような研究は高品質なソフトウェアを開発するために非常に重要です．