「ソフトウェア」の安全性向上を目指し、「プログラム検証」の技術開発に挑む

現代社会のリスクを未然に防ぐ
全自動ツールの開発を目指して

研究の基盤は「数理論理学」。三段論法や背理法など人間の論理的思考を数学的手法により探究する学問です。現在行っている研究のメインテーマは、「数理論理学を用いたプログラム検証」。ソフトウェアは、スマホやパソコン、銀行のシステム、乗り物の制御など現代社会のあらゆる電子機器の中で動作しており、プログラムにより稼働しています。プログラムは人による手作業で作成されるためミスやエラーが出るリスクがあり、それが原因で多大な損害が発生した例は多数あります。そうした誤りを防ぐため、プログラムが仕様通りであるかを確認する作業が「プログラム検証」です。
検証方法は大きく分けて「動的」「静的」の2種あり、私たちは数理論理学を活用した「静的」検証の研究に取り組んでいます。ソフトウェアを実際に作動させて誤りを確認する「動的」検証に対し、「静的」検証は作動前にプログラムの内容を確認しプログラムが「仕様（プログラマの意図）通りであること」を数学的に証明し保証するものです。
この分野には非常に幅広い領域がありますが、私たちの研究はメモリの検証に特化。機械だけで検証作業が進められる「全自動ツール」の開発を進めています。そして私たちは、「プログラム検証」の研究と「全自動ツール」の開発を通じて、現代社会に必要不可欠なソフトウェアの安全性向上に貢献したいと考えています。

目標は、ソフトウェアの安全性の向上。
大きな夢を抱きチャレンジを

研究室では、プログラム検証の研究に加えて、「関数型プログラミング言語理論」「型理論」といった基礎研究色が強い研究も進めています。前者は、再帰を用いた数学的な関数の定義がそのままプログラムになるというもの。その最大の利点は数学との親和性が高いことにあります。関数型プログラミング言語における実際のプログラム作成は、正しさのチェックがしやすい小さな関数をいくつか作り、それらを関数合成によってつなげる手法を取るため、もし問題があったらプログラムを細かく分割して確認できバグが発見できます。後者は整数型やブール型などの多くのプログラミング言語で用いられているデータ型の概念を抽象化した数学的概念で、この型についての性質を研究する理論。どちらも「全自動ツール」にも通じる基礎研究であり、ソフトウェアの安全性向上を目指すものです。
これらの研究は現在、IT系グローバル企業が取り組む研究分野にダイレクトにつながっており、こうした企業では数学のプリミティブな勉強に取り組んだ人材が活躍しています。アイディアと理論的な基盤を持ち合わせていれば、グローバル企業に就職したり、自ら起業したりする道も開けるかもしれません。
課題が多く研究はスムーズに進みませんが、だからこそやりがいのある分野です。まだまだ未開拓で、大きな夢を抱ける研究分野なのです。ぜひ未知のものにチャレンジする気持ちで研究に取り組んでほしいと思います。

木村大輔准教授

理学部情報科学科講師。2001年3月京都大学理学部卒業、2003年3月京都大学大学院理学研究科数学・数理解析専攻（数学）修了、2007年3月総合研究大学院大学複合科学研究科情報学専攻修了（博士〈情報学〉）。2007年4月国立情報学研究所特任研究員、2009年4月東京大学大学院情報理工学研究科研究生、2010年4月国立情報学研究所特任研究員、2015年4月東邦大学理学部非常勤講師を経て2016年4月講師、2023年4月より現職。

研究内容

● 分離論理を用いたプログラム検証
● 関数型プログラミング言語の基礎理論
● 古典論理に内在する計算機構

卒業研究例

● 定理証明支援系Coqを用いた「鳩の巣原理」の証明検証
● 数理論理学における充足可能性問題を解くアルゴリズムを応用した、カードゲーム「アルゴ」の思考ルーチンの作成