セミナーのご案内
日時：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.
問い合わせ先： 鹿島 亮（東京工業大学 数理・計算科学専攻） [email protected]