September 20, 2024
Probabilistic programming is a widely used paradigm to describe stochastic models in the form of executable computer programs. Reasoning about loops is arguably the hardest task in verifying probabilistic programs as it amounts to computing quantitative fixed-point semantics that are highly intractable in practice. In this talk, I present verification techniques to establish sound over- and under-approximations of probabilistic loop semantics as well as techniques to infer the exact semantics for a restricted class of programs. This verification perspective will be briefly complemented by a synthesis one for (semi-)automatically generating quantitative loop invariants.
About Mingshuai Chen
Mingshuai Chen is an Assistant Professor leading the Formal Verification Group (https://fiction-zju.github.io/) at Zhejiang University (ZJU), Hangzhou China. Prior to joining ZJU, he worked as a Postdoctoral Researcher at RWTH Aachen University in Germany. In 2019, he received the Ph.D. degree in computer science from the Institute of Software, Chinese Academy of Sciences. Mingshuai Chen’s research interests include formal verification, synthesis, programming theory, and cyber-physical systems, broadly construed in theoretical aspects of computer science. He has co-authored peer-reviewed papers at flagship journals/conferences including Inf. Compt., IEEE Trans. Automat. Contr., OOPSLA, CAV, FM, ASPLOS, IJCAR, etc. He was the awardee of the Distinguished Paper Award at ATVA 2018, Best Paper Award at FMAC 2019, and the CAS-President Special Award in 2019. Mingshuai Chen is the recipient of the NSFC Excellent Young Scientists Fund Program (Overseas), which is known as one of the most prestigious grants for young researchers across China. His research results have been partially applied in the verification of control programs of the Chinese lunar lander Chang’e-3 and the Chinese high-speed railway system.