応募書類の受付は4月26日13時に締め切りました。
書類の受諾状況は、5月中旬頃に応募者登録サイトに表示されます。
"Application forms were closed at 13:00 on 26 April.
The acceptance status of documents will be displayed on the registration website around mid-May."
Formal Verification of Hybrid Systems with Infinitesimal Programming
Formal verification is a mathematical methodology for ensuring that a system works as intended. It is applied to various kinds of systems including hardware and software. Among them, application to hybrid systems, systems that exhibit both flow (continuous evolution of system parameters) and jump (discrete transition of system parameters) is becoming a hot topic because ensuring that such systems work correctly is critical as many safety-critical systems are managed by software. In this talk, I will first introduce what it is like to verify system correctness “formally”. Then, I will talk about my recent joint work with Ichiro Hasuo (Univ. of Tokyo) on formal verification of hybrid systems based on infinitesimal programming. As much as possible, the seminar content does not assume any knowledge of mathematics and computer science.