2026年7月7日至7月10日，第22届华东师范大学可信软件国际暑期学校在滴水湖国际软件学院顺利举办。本届活动延续“形式化验证与可信AI”主题，汇聚多位国际顶尖领域专家，来自国内外多所高校与科研院所的青年师生齐聚临港，完成为期四天系统、深度的专题授课与学术交流。

自2004年起，华东师范大学可信软件国际暑期学校已连续举办22届，为计算机、软件工程领域青年科研人员与研究生，搭建常态化国际学术交流平台，助力国内可信软件、形式化方法方向的学科建设与青年人才培养。

开幕式现场

本次活动特邀四位国际知名学者全程授课，分别为英国皇家工程院院士、约克大学James Woodcock教授，法国图卢兹大学Yamine Ait Ameur教授，FBK资深研究员Alessandro Cimatti，伦敦南岸大学Jonathan Bowen教授。各位专家围绕主题开展系统性授课，内容兼顾基础理论、前沿动态与工程实践，覆盖无限状态系统分析、智能网联汽车可信验证、Event-B领域建模、形式化方法与人工智能交叉研究等多个热门研究方向。

Alessandro Cimatti 授课

Alessandro Cimatti教授带来基于SMT的无限状态系统分析专题课程，分两日完整讲解SMT求解底层原理、复杂系统建模思路与自动化验证技术实现路径。结合工控、嵌入式等安全关键系统实例，梳理无限状态场景下形式化分析的完整技术框架，为在场师生提供高可靠软件验证的全新研究思路。

Jonathan Bowen 授课

Jonathan Bowen教授开设两大专题内容。其一梳理形式化方法与人工智能融合发展脉络，梳理二者结合的发展历程、现存技术瓶颈与未来研究方向；其二以计算机逻辑领域先驱Tony Hoare的学术生涯为主线，串联程序逻辑、形式规约、软件验证等经典理论体系，夯实学员形式化研究底层理论基础。

James Woodcock 授课

James Woodcock教授聚焦智能网联汽车（ICV）建模与验证，连续两日完整授课。围绕自动驾驶场景的安全核心需求，讲解车规级软件形式化建模规范、风险约束定义、自动化验证全流程，搭配车载系统工程实例，打通形式化理论与智能交通产业落地的研究通道。

Yamine Ait Ameur 授课

Yamine Ait Ameur教授主讲基于Event-B的领域专用形式化建模，清晰区分描述式、规约式两类建模范式，完整演示Event-B工具链搭建、领域模型迭代优化、系统不变式校验实操流程，技术方案可广泛适配工业软件、安全关键控制系统等多种应用场景。

每日课程设置丰富交流场景，每节讲座结束后开放现场提问环节，参会师生结合自身研究方向踊跃发问，授课专家针对性细致解答；茶歇时段同样成为轻松的学术沟通窗口，师生自由围坐交流，围绕大模型形式化校验、自动驾驶安全保障、Event-B工具实操、SMT算法优化等研究难点交换思路，全程研讨氛围轻松浓厚。

暑期学校现场

本次暑期学校为在场青年科研工作者搭建起直面国际前沿理论的学习渠道，推动可信AI、高可信软件领域跨院校、跨国界的学术思想互通。未来，学院将持续引入海外专家进行授课，聚焦可信智能软件研究，打造人才、科创、产教、国际交流综合平台，助力可信软件学科发展。