一句话：将符号执行与概率推理结合，通过模型计数计算程序目标事件的发生概率，用于软件安全与可靠性分析。
该报告探讨如何将符号执行与概率推理相结合，以对程序行为进行概率化分析。符号执行通过收集并求解程序路径上的符号路径条件，一次探索多条程序行为；扩展后的方法计算到达目标程序事件的条件，并利用模型计数（model counting）统计满足这些条件的输入域比例，从而得到事件发生概率。这一概率信息可用于在概率化风况下评估飞机控制器的可靠性，或借助香农熵（Shannon entropy）等信息论指标量化软件系统中敏感数据的泄露。报告回顾相关进展并讨论如何利用该技术保障软件系统的安全性与可靠性。
Summary form only given. Symbolic execution is a systematic program analysis technique which explores multiple program behaviors all at once by collecting and solving symbolic path conditions over program paths. The technique has been recently extended with probabilistic reasoning. This approach computes the conditions to reach target program events of interest and uses model counting to quantify the fraction of the input domain satisfying these conditions thus computing the probability of event occurrence. This probabilistic information can be used for example to compute the reliability of an aircraft controller under different wind conditions (modeled probabilistically) or to quantify the leakage of sensitive data in a software system, using information theory metrics such as Shannon entropy. In this talk we review recent advances in symbolic execution and probabilistic reasoning and we discuss how they can be used to ensure the safety and security of software systems.