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

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

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

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

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

• 原子過程 / 原子・分子の反応プロセス / 粒子同士の衝突・反応 / 宇宙空間での分子形成 / 核融合の制御 / オーロラはなぜ発光するのか / 先端計測装置の開発 / 医療への貢献 / 身のまわりの謎に目を向ける / ヒトの呼気で病気を発見

• ホルモン作用の仕組みを
  “両生類”で明らかに。

  

  

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

  

  

• スマホの進化を支える
  材料開発の最前線。