教員紹介：西田 直樹（にしだ なおき）

研究内容

バグのない高信頼なソフトウェアを作成することは現代社会において非常に重要です。通常はプログラムが正しいことを検証することで高信頼なプログラムを開発します。私の研究では、関数型言語だけでなく命令型言語の計算モデルとも言える制約付き項書換え系を用いて、C言語プログラムが仕様に相当する関数と等価であることを自動証明する研究に取り組んでいます。自動証明には書換え帰納法と呼ばれる人間が行う証明に沿った証明原理を利用しています。この証明法の自動化では、人間がどのように証明を完成させるかという知識を計算モデルの上で形式化します。また、書換え帰納法による検証技術を大学のプログラミング演習で提出されるプログラムが正しいことの検証だけでなく、車載組込み制御システムの検証への応用にも取り組んでいます。その他、与えられたプログラムが定義する関数の逆関数を定義するプログラムを自動生成するプログラム逆化や、可逆計算モデルの研究にも取り組んでいます。

所属・連絡先など

• 情報システム学専攻/コンピュータ科学科情報システム系
• E-mail: nishida@i.nagoya-u-ac-jp
• 居室：IB電子情報館南棟5階589
• 個人HP：https://www.trs.css.i.nagoya-u.ac.jp/~nishida/index-jp.html