该论文由交大电院BASICS实验室博士生王培新，在符鸿飞助理教授的指导和计算机系傅育熙教授的支持下，与奥地利科学技术研究院（IST Austria）和华东师范大学的研究团队合作共同完成。该论文提出了一种自动化的验证算法，可以得到概率程序期望资源消耗的紧凑上下界。
验证结果以及与仿真结果的比较
该论文是研究如何通过自动化的验证算法给出概率程序期望资源消耗的紧凑上下界。相对于先前已有的结果，本论文做出了以下推广。首先能够同时给出紧凑的上下界，而先前结果只能给出一个紧凑上界；其次，能够同时处理正和负的资源消耗，而先前结果只能处理正的资源消耗；除此之外，能够处理一般意义下与程序变量取值相关的资源消耗，而先前结果只能处理常数的资源消耗。为实现这三个主要学术目标，本论文首先给出了经典数学定理Optional Stopping Theorem的一个显著推广，随后基于团队先前关于利用鞅验证概率程序的结果给出了自动化的验证算法。实验结果清晰地表明，此种验证算法在先前已有的实例以及在先前方法无法处理的实例上，都能够得到紧凑的上下界。
PLDI会议全称"ACM SIGPLANconference onProgrammingLanguageDesign andImplementation"，是程序语言和编译技术领域最重要的国际会议。PLDI自1979年创办，今年是第40届，会议平均论文录用率为21%。之前，署名第一完成单位为中国大陆的只有不足10篇论文入选PLDI，近5年（2014-2018）仅有2篇。
论文链接：https://arxiv.org/abs/1902.04659
符鸿飞，上海交通大学约翰·霍普克罗夫特计算机科学中心助理教授。他于2010年赴德国亚琛工业大学计算机科学系攻读形式化方法相关的博士学位，读博期间，符鸿飞主要研究概率系统形式化验证。花费4年时间顺利拿到博士学位之后，符鸿飞开展了博士后研究，和奥地利科学技术研究院（IST Austria）的Krishnendu Chatterjee教授合作研究概率程序的形式化验证，并发表了多篇关于基础理论的结果。
符鸿飞长期致力于探索理论计算机科学中形式化方法领域的理论问题。在理论计算机科学国际著名学术会议上以主要贡献者身份发表论文10余篇；参与国家自然科学基金重点项目1项；获得国家自然科学青年基金资助1项。
王培新，上海交通大学电子信息与电气工程学院2015级博士研究生，现正在计算机系傅育熙教授领导的BASICS实验室（https://basics.sjtu.edu.cn/）攻读博士学位。2011-2015年就读于华东师范大学物理学专业，并取得学士学位。主要研究方向包括概率程序的运行时间，资源损耗，程序敏感性分析等问题。
