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 approach for synthesizing piecewise bounds over probabilistic programs. First, we show how to extract useful piecewise information from latticed $k$-induction operators, and combine the piecewise information with Optional Stopping Theorem to obtain a general approach to derive piecewise bounds over probabilistic programs. Second, we develop algorithms to synthesize piecewise polynomial bounds, and show that the synthesis can be reduced to bilinear programming in the linear case, and soundly relaxed to semidefinite programming in the polynomial case. Experimental results show that our approach generates tight piecewise bounds for a wide range of benchmarks when compared with the state of the art.

翻译：在概率程序分析中，定量分析旨在为期望值和断言概率等概率性质推导严格的数值边界。先前工作大多将整个程序状态空间视为整体来考虑数值边界，而未考虑分段边界。整体边界通常要么过于保守，要么在表达性和简洁性上有所不足。为获得更优边界，我们提出一种合成概率程序分段边界的新方法。首先，我们展示如何从格化$k$归纳算子中提取有效的分段信息，并将该信息与可选停止定理结合，形成推导概率程序分段边界的通用方法。其次，我们开发了分段多项式边界的合成算法，证明在线性情形下该合成可简化为双线性规划问题，在多项式情形下可稳健松弛为半定规划问题。实验结果表明，与现有技术相比，本方法能为广泛基准程序生成严格的分段边界。