研究内容

プログラムはとにかく動けばよいというわけではありません。「どんな入力を与えても必ず停止する」など、開発者の意図したとおりに振る舞うことが重要です。このような性質を満たすことを保証するためには、どうすればよいでしょうか。すべての入力についてテストすればよいと思うかもしれません。入力のドメインが小さい場合はそれもよいでしょう。しかし、一般的には入力は無限にあり、すべてをチェックすることなど到底不可能です。結縁・中澤研究室では、プログラムが特定の性質を満たすことを数理的な手法を用いて証明する研究を行っています。具体的には、モデル検査、抽象解釈、型システムなどについて研究しています。証明と言っても、高校数学のように人間が頭を捻って考えるばかりではなく、コンピュータを使って自動化できることも多くあります。このような研究は高品質なソフトウェアを開発するために非常に重要です。

プログラムを実行するときには、計算が進行するに従って不要となった情報を忘れます。設計通りに動作しなかったときには、その原因は忘れた情報に含まれます。プログラムを可逆的に実行するためには、実行に使われた情報を保存しておく必要があり、実行の際に通常では不要な情報も保存します。可逆計算の概念は、実行として必要十分な情報を定義します。この考えに基づいて、デバッグなどによってソフトウェア、特に、並行性をもつソフトウェアに対する信頼性向上の枠組みを研究しています。

現代の情報社会では、ソフトウェアやAI、通信システムなど、複雑な情報処理を行う技術が広く利用されています。こうしたシステムを正しく理解し、その振る舞いを見通しよく整理するためには、その背後にある記号処理や計算規則を数学的に捉える視点が重要になります。 形式言語やオートマトンは、コンピューターが扱う記号列や計算規則を記述するための数学的モデルです。本研究では、これらの構造を代数学の観点から理解する「代数的言語理論」を扱っています。特に、正則言語のクラスと有限半群のクラスの間には深い対応関係が存在することが知られています。一見すると離れた分野に見える形式言語理論と抽象代数学が、本質的に結びついている点は、この分野の大きな特徴の一つです。 現在は、正則言語のクラスに対して成立するこの対応関係を、文脈自由言語などのより複雑で実用的な言語クラスへ拡張する研究に取り組んでいます。こうした研究を通じて、複雑な言語や計算モデルを統一的・構造的に理解することを目指しています。

実世界で使用されているシステムの多くは、同時並行的に動作する複数のシステムの組み合わせで構成されています。多くの場合、それぞれのシステムは「ある時間までに処理を完了しなければならない」といった時間的な制約を満たす必要があります。これらのシステムがCPUやメモリなどの資源を共有して動作するとき、正しく振る舞うかどうかを調べるのは難しい問題です。結縁・中澤研究室では、“動作の正しさが保証されている”実時間並行システムを“コストを抑えて”開発する手法を研究しています。主な研究分野は、プロセス代数や時間オートマトンなどの形式的手法の基礎理論、およびそれらの形式的手法に基づく開発手法、モデル化、モデル検査、コード生成などです。