[logic-ml] セミナー案内

[KASHIMA Ryo]

セミナーのご案内

日時：4月19日(木)16:30から
場所：東京工業大学 大岡山西８号館W棟11階 W1101セミナー室
会場までの交通案内はこちらから：
http://www.titech.ac.jp/about/campus/index.html

話者：蓮尾 一郎 （東京大学コンピュータ科学専攻）
http://www-mmm.is.s.u-tokyo.ac.jp/~ichiro/
題目：Programming with Infinitesimals: A While-Language for Hybrid System Modeling
(Joint Work with Kohei Suenaga, Kyoto University)
概要：
We add, to the common combination of a WHILE-language and a
Hoare-style program logic, a constant dt that represents an
infinitesimal (i.e. infinitely small) value. The outcome is a
framework for modeling and verification of hybrid systems: hybrid
systems exhibit both continuous and discrete dynamics and getting them
right is a pressing challenge. We rigorously define the semantics of
programs in the language of nonstandard analysis, on the basis of
which the program logic is shown to be sound and relatively complete.
If the time allows, our recent prototype automatic prover will also be
demonstrated.
参考文献：
Kohei Suenaga and Ichiro Hasuo.
Programming with Infinitesimals: A While-Language for Hybrid System Modeling.
Proc. ICALP 2011, Track B. LNCS 6756, p. 392-403. Springer-Verlag.
Ichiro Hasuo and Kohei Suenaga.
Exercises in Nonstandard Static Analysis of Hybrid Systems.
To appear in Proc. CAV 2012.

問い合わせ先：
鹿島 亮（東京工業大学 数理・計算科学専攻）
kashima at is.titech.ac.jp