情報学研究科に着任して

末永 幸平

末永先生写真2013 年10 月に情報学研究科通信情報システム専攻に准教授として着任しました末永幸平と申します。工学部情報学科計算機科学コースを兼坦しております。着任前は京都大学白眉センターに所属しておりました。

私の専門はプログラム検証のための理論です。世の中のあらゆるものがコンピュータとのつながりを持とうとしている現在において、その動作を記述するプログラムには正確性が求められます。特に、自動車や航空機のようないわゆるセーフティクリティカルなシステムにおいては、プログラムの誤りによって人命や財産に多大な影響が出ることもあり、正しいプログラムを作るための技術が重要になっています。

プログラムの誤りを減らすためには、多くの入力で実際にプログラムを動作させてみる、いわゆるソフトウェアテストを行うことが一般的になっています。しかしながら、ソフトウェアテストでは誤りを発見することはできるものの、テストされたプログラムに誤りが存在しないことまでは保証できません。そのため、プログラムに高度な安全性が求められる分野においては、プログラムをどこまでテストすれば十分なのかということが問題になっています。

私の専門であるプログラム検証は、ざっくりと言えば、この問題を「プログラムの正しさを数学的に証明する」というアプローチで解決しようとするものです。この手法では「プログラムが任意の入力について仕様に沿って正しく動作する」という言明を数学的に厳密な命題として記述し、その証明を与えることを試みます。これによりプログラムがすべての入力について仕様通りに動作することを高い精度で保証することが可能となります。

研究のねらい

このような証明をプログラマが手動で与えるのは難しいので、できるだけ証明を自動的に発見するための手法が多く研究されています。もちろん、任意のプログラムと任意の仕様について正しい証明(あるいは反例)を自動的に与えることは不可能なので、プログラムのクラスを限定する、特定の仕様についての検証手法を設計する等のアプローチを取ることが多いです。私の最近のメインのテーマは、このようなソフトウェアのための自動検証手法を、ハイブリッドシステムと呼ばれる連続遷移と離散遷移を両方含むプログラムに適用することです。

また、教育面では情報学科計算機科学コースの授業を担当しております。着任以来新しい授業の立ち上げにも参加させて頂いており、今学期は2 回生配当科目である「計算機科学のための数学演習」の立ち上げに携わりました。この科目は数学を用いたレポートや研究成果等のコミュニケーション能力の向上を目的として立ち上げられたもので、学生が実例を通じて様々な形をした命題の証明技法を学びつつ、厳密な論理に基づいた文章を書けるようになることを目標としております。初年度で手探りの授業になったこともあり、まだ改善点が多いように感じていますが、授業内で行う演習や毎回出題する宿題への解答を見る限り、学期始めに比べて学生の論理的に数学的文章を書く能力が上がっているのを感じます。

このように、着任以来研究教育両面で充実した日々を送らせていただいております。大学を取り巻く環境は様々な面で変化しつつあると言われておりますが、そのような中にあって新時代の京都大学の歴史を積み上げることに少しでも貢献できるように研鑽したいと考えております。

(情報学研究科 准教授)