Presenter: Shenghua Feng
Abstract: Formal verification is the only proven method for ensuring that a system is completely free of programming errors. By providing a mathematical proof, it guarantees that an OS kernel performs as expected under all possible conditions. In this talk, we will outline a general framework for OS verification and share our hands-on experience in verifying the functional correctness of the OpenHarmony LiteOS-m kernel.
Bio: Shenghua Feng is currently an Assistant Researcher at Zhongguancun Laboratory. He obtained his Ph.D. from the Institute of Software, CAS in 2023, and a B.E. in Math from Nanjing University in 2018. His primary research interests lie in formal verification, with a particular emphasis on the analysis, verification, and synthesis of programs and hybrid systems. He has published several papers in leading conferences including CAV, OOPSLA, FM, and IEEE TAC.