Presenter: Shenghua Feng
Abstract: In probabilistic program analysis, quantitative analysis aims at deriving tight numerical bounds for probabilistic properties such as expectation and assertion probability. Most previous works consider numerical bounds over the whole program state space monolithically and do not consider piecewise bounds. Not surprisingly, monolithic bounds are either conservative, or not expressive and succinct enough in general. To derive better bounds, we propose a novel k-induction based approach for synthesizing piecewise bounds over probabilistic programs.
Bio: Shenghua Feng is an Assistant Researcher at the Institute of Software, Chinese Academy of Sciences. His primary research interests lie in the formal verification and synthesis of programs and hybrid discrete-continuous systems, with a particular focus on reasoning about programs and hybrid systems.