3月15日13時に第15期公募情報を公開いたしました。
4月1日13時より応募者登録サイトへの登録が可能です。
Information on the 15th call for applications was opened at 13:00 on 15 March.
Applicants can register on the registration website from 1 April at 13:00.
『無限小プログラミングによるハイブリッドシステムの形式検証』
形式検証はシステムが意図通りに動作することを数理的手法によって保証するための手法である。この手法は現在ハードウェアやソフトウェア等の様々なシステムに適用されている。中でもハイブリッドシステム(物理量の変化による連続的なシステムの挙動とソフトウェアの動作による離散的な挙動が含まれるシステム)への形式検証の適用は、ハイブリッドシステムに非常に高度な安全性が求められることもあり、活発な研究分野となっている。今回のセミナーでは、まず初めに「形式的に」システムの正しさを証明するとはどういうことかを紹介し、その後話者と東京大学の蓮尾一郎氏との研究である無限小プログラミングに基づくハイブリッドシステム検証手法を紹介する。参加者の数学と計算機科学に関する前提知識は(できるだけ)仮定しない。