Title: Extending Hoare Logic to Hybrid Systems
Speaker: Naijun Zhan (Peking University)
Time: 2025/12/9 (Tuesday) 15:10-18:00
Location: Room 211, Natural Sciences Teaching Building (理教), Peking University
Abstract:
In this talk, I will talk about our efforts on extending Hoare logic to hybrid systems, named hybrid Hoare logic, including two versions: a DC-based version and a generalized version without DC. I will briefly introduce the DC-based version, and mainly focus on the second version. I will explain why we need a generalized version, and present its proof system, the soundness and discrete and continuous relative completeness of the proof system, the implementation of an interactive theorem prover based on Isabelle/HLL called HHL Prover, the automation of HHL Prover, and finally introduce some applications with the logic and its prover.
Biography:
Naijun Zhan is a Boya distinguished professor in the School of Computer Science of Peking University. He got his bachelor degree and master degree both from Nanjing University, and his PhD from Institute of Software Chinese Academy of Sciences (ISCAS). Prior to join Peking University, he worked at ISCAS as an associate professor, a full professor, and a distinguished professor. Before that, he worked at the Faculty of Mathematics and Informatics, Mannheim University, Germany as a research fellow, and afterwards. His research interests cover formal design of real-time, embedded and hybrid systems, program verification, and so on. He is in the editorial boards of Journal of Automated Reasoning, Formal Aspects of Computing, Journal of Logical and Algebraic Methods in Programming, Journal of Software, Journal of Electronics, and Journal of Computer Research and Development and so on, a member of the steering committees of SETTA and MEMOCODE, the pc co-chairs of TACAS 2027, FM 2021, SETTA 2016, the general co-chairs of MEMOCODE 2018, MEMOCODE2019 and ICESS 2019, and serves more than 100 international conferences program committees e.g., CAV, RTSS, HSCC, FM, TACAS, EMSOFT and so on. He published more than 150 papers in international leading journals and conferences and 2 books, and edited 5 conference proceedings and 8 journal special issues. See https://lcs.ios.ac.cn/~znj/ for more details.
