概率程序的符号语义（扩展版）
摘要：基于观察语句和从连续分布进行采样的概率程序，我们提出了一种新的符号执行语义。在Kozen的重要工作基础上，这种符号执行语义由可数个可测函数和状态空间分区组成。我们使用这种新的语义来为概率程序的符号执行提供完整的正确性证明。我们还在工具symProb中实现了这种语义，并通过示例说明其用法。
作者：Erik Voogd, Einar Broch Johnsen, Alexandra Silva, Zachary J. Susag, Andrzej Wk{a}sowski
论文ID：2307.09951
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-07-20