2025年6月30日至7月4日，第21届华东师范大学可信软件国际暑期学校——形式化验证和可信AI在滴水湖国际软件学院成功举办。

开放共享，薪火相传。自2004年起，华东师范大学可信软件国际暑期学校已连续举办21届，为融通东西方软件工程领域学术交流，推动我国软件学科创新发展，培养具有国际竞争力的青年软件人才作出了重要贡献。

本期暑期学校以"形式化验证与可信AI"为主题，吸引了来自华东师范大学、北京大学、上海交通大学、国防科技大学、电子科技大学、中国科学院软件研究所、中国地质大学、阿姆斯丹大学等国内外知名高校的60余名师生参加。

新加坡国立大学的董劲松教授、英国牛津大学的Giuseppe De Giocoma教授与Nobuko Yoshida教授、瑞典查尔姆斯理工大学John Hughes教授和美国莱斯大学的Moshe Vardi教授受邀为学生授课。五位专家聚焦“形式化验证与可信AI”前沿领域，系统阐释了理论框架与方法体系，并结合实际案例展示了创新应用成果。

董劲松教授在"可信AI与超越大模型的推理"专题课程中，深入剖析了大型语言模型（LLM）在软件工程应用中的技术边界。创新性地提出采用程序精化演算法构建形式化思维链，以验证LLM生成代码的正确性。课程还探讨了LLM辅助系统设计的新范式，引入增强型形式化方法智能体（Enhanced Formal Methods Agent）概念，并通过案例分析揭示了LLM在策略推理方面的固有局限，系统论证了形式化方法在可信AI体系中的核心价值。

Giuseppe De Giocoma教授针对线性时态逻辑在AI领域的应用，详细介绍了有限语义上的合成（synthesis）技术。他系统性地阐释了近年来在该领域取得的最新研究成果，包括：基于确定有限自动机（DFA）的合成技术、面向不确定环境的合成方法，以及基于past时态逻辑的合成算法等。同时，他也前瞻性地指出，该研究方向在机器人任务规划领域具有广阔的应用前景。

Nobuko Yoshida教授通过构建'理论推导-实例验证-实践应用'的三维教学框架，拆解会话类型进化史。从最基础的二元会话不变式，到复杂的多方通信协议验证，再到Rust语言中利用线性类型实现会话安全，她将抽象的会话演算转化为可操作的编程范式，使同学们切实掌握会话类型在实际开发中的应用技巧。

John Hughes教授以生动幽默的教学风格，系统阐释了基于性质测试（Property-based Testing）的方法论体系。课程以Haskell语言为实践载体，深入剖析了该技术的核心原理，包括：性质规约（property specification）的数学定义、随机输入生成器（randomized input generator）的构造方法，以及面向智能合约等状态型系统的适应性扩展。通过工业级复杂系统的实证案例，直观展示了该测试范式的工程应用价值。

Moshe Vardi教授首先系统梳理了逻辑学在计算机科学领域的历史沿革与应用谱系，继而从逻辑表达力与计算复杂性等维度，深入剖析了计算机逻辑研究的演进路径。Moshe Vardi教授系统性地阐释了逻辑学在各领域的应用演进与未来发展图景，他从形式化验证与数据库理论的奠基性研究出发，延伸至计数（counting）与采样（sampling）方法，最终拓展到人工智能前沿领域。

本期暑期学校创新设立"AI与形式化方法"圆桌论坛，特邀5位授课专家与华东师范大学软件工程学院（滴水湖国际软件学院）外籍教师Jeff Sanders同台论道，围绕AI形式化验证、可信系统构建等前沿议题展开深度对话，与会师生积极互动。

华东师范大学可信软件国际暑期学校为青年学者搭建了一个国际化高端学术的对话体系，彰显了该领域融合创新、开放发展的学科生态。

面向未来，滴水湖国际软件学院将持续深耕学术前沿，聚焦安全可信智能软件与系统领域，构建国际专家临港授课长效机制，以全球化视野建设人才培养新高地，为世界软件工程领域输送更多具有国际竞争力的卓越人才，架设东西方学术交流的坚实桥梁。矢志打造拔尖软件人才培养基地、软件技术一流创新基地、关键软件产教融合中心、国际学术资源汇聚中心！