新任教員の紹介 [プログラミング言語理論，ソフトウェア検証]

この記事では2020年4月1日に数理・計算科学系に着任された佐藤哲也助教にフォーカスします。

【研究内容】
プログラムの表示的意味論と形式的検証に関する、理論的研究を進めています。表示的意味論とはプログラムの数学的モデルで、直観的に言えばどのような関数として表されるかを記述したものです。形式的検証とは、プログラムの仕様を形式的に記述し、その正しさをチェックすることで、誤りのない検証を行う手法です。例えば、プログラムの入出力に関する条件を論理式で記述し、その論理式が正しいことの証明を与えることで、プログラムが所望の条件を満たすことを保証するという具合です。
確率的なふるまいをするなど、挙動がより複雑なプログラムについて、表示的意味論がどうなって、形式的検証をどのように行えばよいかを調べています。

【最近の研究トピック】
最近は、差分プライバシーと呼ばれるプライバシー手法について研究もしています。差分プライバシーはデータベースの出力にノイズを加えることで、データベースに格納された個人情報を保護するという手法です。既に広く実用化されていますが、まだまだ発展の余地があります。
人の手で差分プライバシーをチェックするのは難しいので、そこに形式的検証の手法を使います。検証手法を改善し、より効果的な検証が行えるようにすることに興味を持っています。
また、確率的なふるまいをするプログラムの数学的モデル自体にも興味を持っています。

【学生へのメッセージ】
ぜひ、学生生活を楽しんでください。
私の研究にもし興味があればぜひお気軽に声をかけてください。

• 佐藤哲也助教のホームページはこちら