夜雨聆风
TASE 2026
为促进软件工程理论、形式化方法、人工智能安全、程序验证与可信系统等方向的国际学术交流，第20届软件工程理论方面国际研讨会(The 20th International Symposium on Theoretical Aspects of Software Engineering,TASE 2026) 于7月4日至6日在我院举行。TASE会议2007年首届、2016年第十届均由我校承办，时隔十年，第二十届会议再度落地华东师大，我校有幸见证会议发展历程中的三个重要里程碑节点。
本届会议由我院蒲戈光教授担任大会主席，牛津大学Giuseppe De Giacomo教授、我院李建文教授担任程序委员会共同主席。会议汇聚全球软件工程、形式化方法、可信AI、程序验证领域顶尖学者，三天议程覆盖形式化验证、大模型软件工程、定量概率分析等前沿方向，同时设立海外知名专家特邀报告、主题报告分享、纪念专题研讨等多个环节，搭建起覆盖理论、工具、应用多层次的国际化学术交流平台。
TASE是形式化软件工程领域极具代表性的国际学术会议，位列CCF推荐国际会议名录，历经二十届持续深耕理论软件研究，先后在国内外多座城市巡回举办，形成稳定的全球学术交流网络。本届会议论文集由国际知名学术出版机构Springer以计算机科学讲义系列出版，优质成果可推荐至权威期刊《Science of Computer Programming》刊发特刊，长期为全球相关领域学者提供高质量成果发布与学术互通渠道，在程序验证、可信系统、网络物理系统等细分方向具备广泛行业认可度与学术辐射力。
特邀报告
本届会议邀请来自意大利特伦托布鲁诺・凯斯勒基金会、新加坡管理大学、南安普顿大学和牛津大学的四位专家学者进行特邀报告分享。围绕铁路联锁系统形式化设计、可信AI Agent构建、网络物理系统建模分析、复杂程序与系统验证等前沿方向，四位嘉宾结合各自研究积累，展示了形式化方法与软件工程理论在复杂系统建模、分析、验证与保障中的最新探索。
Keynote 1: The OPERA Framework: Formal Design of Railways Interlocking Systems
Fondazione Bruno Kessler的Alessandro Cimatti教授以铁路联锁系统的形式化设计为切入点，在“The OPERA Framework: Formal Design of Railways Interlocking Systems” 报告中介绍OPERA框架的相关研究。报告围绕遗留继电器联锁系统的分析、逆向工程、规约建模与验证展开，展示模型化方法在铁路联锁系统维护、改造与安全保障中的应用价值。
▲Alessandro Cimatti (Fondazione Bruno Kessler, Italy)
Keynote 2: Building Trustworthy AI Agents: Challenges and Attempts
面对大语言模型与智能体系统快速发展的新趋势，新加坡管理大学Jun Sun教授 在“Building Trustworthy AI Agents: Challenges and Attempts”报告中回应可信AI Agent构建中的关键挑战。报告关注 AI Agent 在推理、规划和自主决策过程中的安全性、可靠性与可信性问题，并结合高风险和安全关键应用场景，分析面向大规模AI系统的安全保障方法与开放理论问题。
▲Jun Sun (Singapore Management University)
Keynote 3: Abstraction and Refinement for Modelling and Analysis in Cyber Physical System Design
英国南安普顿大学Michael Butler教授在 “Abstraction and Refinement for Modelling and Analysis in Cyber Physical System Design”报告中，从抽象与精化的视角探讨网络物理系统设计中的建模与分析问题。报告围绕安全规约、环境模型、验证器、系统不变式和精化方法等内容展开，并进一步讨论自治系统和学习型控制系统对传统危害分析方法带来的新挑战。
▲Michael Butler (University of Southampton)
Keynote 4:Neural Proofs for Sound Verification of Complex Programs and Systems
牛津大学Alessandro Abate教授围绕神经证明在复杂程序与系统验证中的应用展开分享。其报告“Neural Proofs for Sound Verification of Complex Programs and Systems”介绍如何构造用于形式化验证与控制的可靠证明，内容涉及概率反应式程序、随机动态系统、证明规则、归纳式证书构造、神经网络训练以及SMT查询，并进一步讨论序贯决策问题中的策略、控制器生成与时序规约实现。
▲Alessandro Abate (University of Oxford)
专题报告
除特邀报告外，TASE 2026还设置多场专题论文报告，集中展示软件工程理论与实践创新的最新成果。会议首日围绕 “Formal Verification and Model Checking、Program Verification and Theorem Proving、Programming Languages and Semantics”等主题展开交流。相关报告涉及自修改代码模型检测、线性时序动态逻辑符号模型检测、实时目标下的 timed games、C 程序定理证明接口、基于分离逻辑的 C 程序验证工具、C 到安全 Rust 的转换框架及时序性质定量评估等方向，体现了形式化方法在程序分析、系统建模与验证工具建设中的持续深化。
DAY 1: Formal Verification and Model Checking、Program Verification and Theorem Proving、Programming Languages and Semantics
▲向右滑动查看更多图片
会议第二天重点关注“AI for Software Engineering and LLM-based Methods、Testing, Fuzzing and Dynamic Analysis、Runtime Analysis and Systems”等方向。与会学者围绕大语言模型辅助需求与形式规约追踪、Rust 程序证明合成、Simulink 模型测试、形式规约辅助代码审查、深度强化学习智能体测试、正则表达式测试、DNN分布感知模糊测试、线程共享动态分析、NAND Flash存储系统管理以及浮点错误检测等议题展开报告与讨论。当天还设置了纪念Jean-Raymond Abrial的专题环节和会议晚宴，为与会者提供了进一步交流思想、拓展合作的机会。
DAY 2: AI for Software Engineering and LLM-based Methods、Testing, Fuzzing and Dynamic Analysis、Runtime Analysis and Systems
▲向右滑动查看更多图片
会议第三天围绕 “Quantitative Verification and Probabilistic Analysis、Tools, Frameworks and Applications、Security and Formal Assurance” 等方向继续开展深入研讨。报告内容覆盖组合式操作语义、安全关键驾驶场景统计模型检测、IoT协议定量韧性分析、带时序依赖目标的增量强化学习、定量自动机生成、相容逻辑转换系统工具、分布式系统场景匹配、Rust物理内存分配器形式化验证，以及量子计算相关实现的语义验证等前沿议题。会议最后举行闭幕环节，对本届会议的学术交流成果进行总结。
DAY 3:Quantitative Verification and Probabilistic Analysis、Tools, Frameworks and Applications、Security and Formal Assurance
▲向右滑动查看更多图片
▲Best Paper Award
本次国际顶尖学术会议的顺利举行，充分印证并显著提升了我校在软件工程、形式化方法、可信智能系统领域的国际学术话语权与行业影响力，同时依托学院 “产教融合、科教融汇” 办学特色，为全球软件工程领域专家搭建起了成果共享、思想碰撞、长期合作的国际化交流桥梁，将有力推动我校软件学科前沿研究、人才培养与国际合作协同发展，为国内可信软件与智能系统领域研究创新注入强劲动力。
文 | 李建文 潘丹 宛宁静
图 | 潘丹 周智琳 宛宁静
编辑 | 宛宁静
审核 | 苏 亭 朱 丹 李建文
