第39回白眉セミナー ： 『無限小プログラミングによるハイブリッドシステムの形式検証』
- 末永 幸平（京都大学次世代研究者育成センター）
- 2012/05/01 4:00pm
- 次世代研究者育成センター(iCeMS西館2階 会議室)
- 日本語
要旨
形式検証はシステムが意図通りに動作することを数理的手法によって保証するための手法である。この手法は現在ハードウェアやソフトウェア等の様々なシステムに適用されている。中でもハイブリッドシステム（物理量の変化による連続的なシステムの挙動とソフトウェアの動作による離散的な挙動が含まれるシステム）への形式検証の適用は、ハイブリッドシステムに非常に高度な安全性が求められることもあり、活発な研究分野となっている。今回のセミナーでは、まず初めに「形式的に」システムの正しさを証明するとはどういうことかを紹介し、その後話者と東京大学の蓮尾一郎氏との研究である無限小プログラミングに基づくハイブリッドシステム検証手法を紹介する。参加者の数学と計算機科学に関する前提知識は（できるだけ）仮定しない。