Invariant Generation by Constraint Solving in Verification of Programs and Hybrid Systems
Speaker
Naijun Zhan,Institute of Software Chinese Academy of Sciences
Time
2020-09-28 10:00:00 ~ 2020-09-28 11:30:00
Location
Room 1319, Software Expert Building
Host
Hongfei Fu
Abstract
Invariant Generation plays a central role in the verification of programs and hybrid systems. As the constraint solving techniques advance rapidly in recent years, constraint solving based invariant generation becomes more and more promising and has been successfully applied to verification of programs and hybrid systems. In this talk, I will report some recent progresses on invariant generation by constraint solving and discuss some remaining challenges.
Bio
Naijun Zhan is a research professor of Institute of Software Chinese Academy of Sciences (ISCAS). He got his bachelor degree and master degree both from Nanjing University, and his PhD from ISCAS. Prior to join ISCAS, he worked at the Faculty of Mathematics and Informatics, Mannheim University, Germany as a research fellow. His research interests cover formal design of real-time, embedded and hybrid systems, program verification, concurrent computation models, modal and temporal logics, and so on. He is in the editorial boards of Formal Aspects of Computing, Journal of Logical and Algebraic Methods in Programming, Journal of Software, and Journal of Computer Research and Development, a member of the steering committees of SETTA and MEMOCODE. He published more than 100 papers in international leading journals and conferences, 2 books and 4 book chapters, and edited 4 conference proceedings and 2 journal special issues. Seelcs.ios.ac.cn/~znj for more details.