近年来，安全攸关软件系统发展呈现出开放性、智能化、人机物融合等新趋势，涉及开放、并发、多变的计算和运行环境，数据驱动的学习赋能部件，以及量子计算、近似计算等新型计算范式，这些新特性在数据、模型、逻辑、算法、实现等多个系统层面引入了高度的随机性和不确定性，影响着软件系统设计、开发、测试、维护等各个阶段，为其可靠性保障带来了巨大挑战。

不确定性软件理论与工程论坛围绕泛在智能时代下软件系统面临的不确定性问题，邀请软件理论与工程领域的国内外专家学者，分享最新的研究成果和实践经验，共同探讨面向不确定性的安全攸关系统质量和可靠性保障方法。本论坛设置两个主题：主题一关注不确定性感知的软件工程，探讨如何有效地识别、度量、建模和处理软件工程各阶段的不确定性，并探索相关成果在自动驾驶系统等复杂软件系统中的应用；主题二关注非确定性系统的形式化验证，探讨概率编程、量子程序等非确定性模型上的定量验证与自动推理方法，并探索相关成果在近似计算、量子计算及人工智能与机器学习等领域的理论与应用价值。

01

论坛组织委员会

陈明帅（浙江大学）

符鸿飞（上海交通大学）

潘敏学（南京大学）

王迪（北京大学）

岳涛（北京航空航天大学）

02

论坛议程

03

论坛报告嘉宾简介

李昂生

报告题目：不确定性中的可定义性原理

报告摘要：

现有的科学体系是牛顿开创的物理世界的科学体系，研究现实世界的物理性质。经典数学对标物理世界科学体系。计算机研究用机器解决现实世界的问题。计算机主要是信息世界的现象。物理世界对象是可分的，物理世界的总方法是分而治之，分而治之的数学原理是微积分。微积分支撑物理世界研究。现实世界由确定性和不确定性构成。现实世界的一个对象可以是任何对象，例如细胞，基因，人，动物，公司，国家等。现实世界的每一个对象都是一系列确定性和不确定性联合作用生成的结果。经典数学的数与形已经不足于建模信息世界的对象。信息科学揭示确定性、不确定性、确定性到不确定性的转化，不确定性到确定性的转化的规律。我提出信息世界的层谱抽象可定义性原理，以建模信息世界的对象。这个报告，我介绍两个概念，物理世界和信息世界的科学概念，介绍信息世界的层谱抽象可定义性原理。

报告人简介：

北京航空航天大学教授。2003年国家杰出青年基金获得者，2008年中国科学院百人计划入选者。现任中国人工智能学会人工智能基础专业委员会主任。1993年中国科学院软件研究所研究生毕业，获博士学位。1993年7月-2018年7月在中国科学院软件研究所工作，分别于1995，1999年被聘为副研究员、研究员。分别于1998年1月-1999年1月，2000年2月-2002年2月在英国leeds大学做访问学者、研究员。2008年9月-2009年3月在美国cornell大学做访问科学家。2012年1月-2012年3月，英国剑桥大学牛顿数学研究所做访问学者。2018年7月-今，入职北京航空航天大学计算机学院。2016年，提出编码树的概念、结构熵的度量，创立了《结构信息论》。2016年以后，提出信息世界的层谱抽象科学范式，建立了包括信息演算理论、信息生成原理和信息解码原理为三大支柱的信息的数学原理；建立了包括（观察）学习的信息理论、自我意识的信息理论和博弈/谋算理论为三大支柱的人工智能信息科学原理。目前主要研究孙子兵法的科学原理。

李重

报告题目：基于不确定性感知的智能模型测试用例选择

报告摘要：

随着人工智能技术的发展，智能模型在各类应用场景中起到越来越重要的作用，如何有效地测试智能模型以保障其安全可靠成为亟待解决的重要问题。测试智能模型需要大量带精确标签的测试用例，而测试用例的标注通常依赖于领域专家进行。为了降低测试用例标注成本，提升智能模型测试的效率，我们首先基于数据间距离、模型训练时动态信息等提出了一系列用于度量测试用例不确定性的方法。在此基础上，我们进一步将这些不确定性度量方法应用到智能模型的测试用例选择中。在不同模型结构以及不同类型测试数据上的大规模实验展示了我们所提出方法的有效性，这些方法选择得到的测试用例不仅可以有效揭示智能模型错误行为同时也可有效用于提升智能模型性能。

报告人简介：

李重，南京大学毓秀青年学者。2023年于南京大学获得博士学位，主要研究方向包括智能软件工程、可信人工智能等。近年来在相关研究领域的重要会议和期刊，如icse、ase、issta、icml、tosem、tse等，发表学术论文10余篇。主持国家自然科学基金青年项目与江苏省青年基金项目，参与国家重点研发计划课题与自然科学基金重点项目等。

张曼

报告题目：应对微服务不确定性的智能测试

报告摘要：

微服务架构作为企业数字化、智能化转型升级的重要途径，已经广泛应用于生物医疗、智慧交通、金融等多个关键领域。然而，由于微服务系统内各个服务之间复杂的依赖关系和系统架构固有的动态、异构及分布式特性，“不确定性”已成为微服务系统的基本特征。如何识别并有效应对这种不确定性，已经成为微服务测试的重要挑战。本报告主要探讨微服务系统的不确定性、识别的方法及应对的手段，包括利用智能测试技术进行动态分析、测试用例生成等策略。

报告人简介：

研究方向涉及复杂软件（如微服务系统、物联网系统）测试、不确定性软件工程、模型驱动工程、及实证软件工程。已参加多项国际科研项目（如欧盟“地平线2020”），在tosem、tse、ese、ase等领域旗舰期刊/会议上发表学术论文30余篇。现任science of computer programming (scp)期刊编委，曾任sosym期刊models2019特刊客座编辑，以及ase research track (ccf-a)、issta research track （ccf-a）、tse (ccf-a)、tcad (ccf-a)、ese、jss、ist和sosym等国际会议和期刊的审稿人。

冯元

报告题目：非确定性量子程序的语义、精化与验证

报告摘要：

非确定性选择是一种有效的程序构造方法，能够描述程序的行为而无需详细说明所有可能的实现。这种构造支持程序的逐步精化，已在软件开发中证明了其有效性。我们提出了一种非确定性量子程序的指称语义，这种语义与概率环境中的提升模型相似。我们进一步研究了非确定性量子程序的验证问题，其中属性由相关希尔伯特空间上的一组厄米算符来定义。我们设计了用于部分正确性和完全正确性的hoare逻辑系统，并证明这些系统在对应的语义正确性方面是可靠且相对完备的。为展示这些证明系统的应用价值，我们对一些量子算法进行了分析，包括量子纠错方案、deutsch算法以及非确定性量子行走。

报告人简介：

冯元，清华大学教授。曾任悉尼科技大学工程与信息技术学院高级讲师、副教授、教授，主要从事量子计算与量子信息处理、量子模型检测、量子程序验证、量子通信并发系统等方面的研究。已出版量子模型检测领域第一本学术专著（剑桥大学出版社），在国际权威期刊和会议发表学术论文100余篇。现任acm transactions on software engineering and methodology编委。曾获全国百篇优秀博士论文奖、澳大利亚研究理事会future fellowship，2023年入选国家海外高层次人才计划。

prof. amir goharshady

报告题目：sound and complete witnesses for template-based verification of ltl properties on polynomial programs

报告摘要：

in this talk, we consider the classical problem of verifying programs with respect to formal specifications given in the linear temporal logic (ltl). we first present sound and complete witnesses for ltl verification over imperative programs. our witnesses are applicable to both verification (proving) and refutation (finding bugs) settings. we then consider ltl formulas in which atomic propositions can be polynomial constraints and turn our focus to polynomial arithmetic programs, i.e. programs in which every assignment and guard consists only of polynomial expressions. for this setting, we provide an efficient algorithm to automatically synthesize such ltl witnesses. our synthesis procedure is both sound and semi-complete. finally, we present experimental results demonstrating the effectiveness of our approach. this talk is based on a recent paper at fm 2024.

报告人简介：

amir goharshady is an assistant professor of computer science and mathematics at the hong kong university of science and technology (hkust). his research is focused on formal program verification, program analysis and parameterized algorithms. amir is due to join the university of oxford in early 2025. he leads the alpacas research group. more information can be found at https://amir.goharshady.com/group.

杨腾舜

报告题目：基于多项式求解的贝叶斯概率程序的后验分布推断

报告摘要：

贝叶斯概率程序是一类带有score（或者observe）语句来表示条件的概率程序，其一大核心问题是如何推断程序所表示的归一化后验分布（npd）。现有的近似算法，比如马尔可夫蒙特卡洛（mcmc）和变分推断（vi）等，无法在有限的时间内产生有保证的结果，而另一类精确推理的方法要么有语法限制，要么无法保证在一般情况下能够成功推理。在这项工作中，我们提出了一种全新的自动化方法，通过多项式求解来推断npd的有严格保证的边界。针对不同类型的贝叶斯概率程序，我们分别提出基于格不动点理论的定理和可选停时定理（ost）的一类乘法变种作为理论基础。我们使用多项式求解来实现我们的不动点定理和ost变种的算法，并且使用截断操作来提高求解精度。在算法的泛用性上，我们的方法可以处理具有无界while循环和具有无穷范围支撑集的连续分布的贝叶斯概率程序。实验结果表明，我们的算法相比于已有的方法更省时，且能够生成接近的甚至更紧凑的npd界限，另外我们的算法能够突破已有方法的语法限制，处理更多的贝叶斯程序。

报告人简介：

杨腾舜，中国科学院软件研究所博士生，师从詹乃军教授，与符鸿飞教授长期合作，研究领域为形式化方法。研究方向包括概率程序的形式化验证，分析和生成等理论，还有概率程序的应用，不变量生成等等。他的研究聚焦于对概率程序的定量性质，包括但不限于期望运行时间，累积资源消耗，期望性质等进行形式化的定量分析，概率程序在贝叶斯模型的应用，即贝叶斯概率程序的分析，还有基于模板的算法中多项式优化理论的应用等等。博士期间以第一及共一作者身份在pldi，jsa等知名会议期刊上共发表文章4篇。

04

论坛组织委员会简介

论坛主席：陈明帅

个人简介：

陈明帅，浙江大学研究员、博士生导师、启真学者，ccf形式化方法专委通讯委员，杭州市钱江特聘专家，国家优秀青年基金（海外）获得者。主要研究方向包括形式验证、程序理论、概率/量子系统、信息物理融合系统等，与合作者一起，提出新型安全攸关系统形式验证理论，解决了概率程序不动点估计、微分系统可达性判定、时滞系统高效控制生成等若干软件理论难题，研究成果应用于我国探月二期工程“嫦娥”三号等重大工程，在inf. comput.、oopsla、cav、fm、asplos等领域旗舰期刊/会议上发表学术论文30余篇，曾获中科院院长特别奖、atva杰出论文奖、fmac最佳论文奖。

论坛主席：符鸿飞

个人简介：

符鸿飞，上海交通大学副教授，ccf形式化方法专委执行委员。长期从事形式化方法前沿理论的研究。在概率系统以及概率程序形式验证的基础数学理论与算法方面贡献丰富，在popl、pldi、cav等程序语言与形式化方法著名国际学术会议与期刊上发表29篇学术成果。提出非确定性概率程序终止性验证的鞅理论框架，并通过线性以及多项式约束求解方法给出概率程序终止性检验算法。提出概率程序灵敏性验证的鞅理论框架。首次通过显著推广经典的鞅停时定理并由此解决概率程序资源消耗的定量分析问题。针对概率程序的断言分析问题建立不动点理论刻画并通过凸优化给出第一个求解指数不动点的完备算法。通过鞅理论的约束求解给出了概率递归关系尾概率分析的新方法，并显著改进karp经典方法所导出的渐进尾概率上界。发表概率程序终止性验证专著章节，由著名出版社剑桥大学出版社出版。

论坛主席：潘敏学

个人简介：

潘敏学，南京大学教授，ccf系统软件专委执行委员。研究工作围绕复杂软件系统的可信保障问题，集中在软件建模与验证、程序分析与测试、智能软件工程等领域；入选国家级青年人才计划、江苏省“青蓝工程”、南京大学“紫金学者”人才计划；主持并参与国家重点研发计划课题、国家自然科学基金、江苏省重点项目等多个科技项目和华为、腾讯等企业技术攻关项目；在tosem、tse、issta、icse、fse、ase等国际顶级期刊会议及中国科学、软件学报等国内优秀期刊发表论文70余篇，获得发明专利与知识产权30余项，6项实现成果转化；获nasac青年软件创新奖（2023）、acm sigsoft杰出论文奖（issta 2020）。

论坛主席：王迪

个人简介：

王迪，北京大学研究员，计算机学院助理教授、博士生导师，ccf形式化方法专委执行委员，国家优秀青年基金（海外）获得者。本科毕业于北京大学，博士毕业于美国卡内基梅隆大学，专注于程序设计语言的理论研究和跨领域应用，主要研究兴趣包括形式化验证、程序分析、类型理论以及概率编程。主持国家优秀青年科学基金项目（海外），研究项目涉及资源安全的系统编程、可编程贝叶斯推断、量化程序分析以及面向证明的编程语言 。研究成果发表于popl、pldi、icfp等程序语言领域著名国际学术会议。

论坛主席：岳涛

个人简介：

岳涛，北京航空航天大学教授，博士生导师。研究方向包括软件测试、不确定性软件工程、模型驱动工程、数字孪生技术、量子软件工程。在国际期刊和会议发表学术论文170余篇。现担任acm transactions on software engineering and methodology（tosem）-- 量子软件工程（qse）专栏主编；国际期刊《ieee transactions on software engineering》、《acm transactions on software engineering and methodology》、《empirical software engineering》和《software and system engineering》编委；曾担任多个国际会议的程序委员会联合主席：models 2019、ease 2021、ssbse 2023等。