No.39 Seminar ： Formal Verification of Hybrid Systems with Infinitesimal Programming
- Kohei SUENAGA（The Hakubi Center）
- 2012/05/01 4:00pm
- The Hakubi Center (iCeMS West Wing 2F, Seminar Room)
- Japanese
Summary
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.