为促进人工智能、形式化方法与软件工程多学科交叉交流,近日,“AI&FM&SE”人工智能、形式化方法与软件工程学术研讨会在滴水湖国际软件学院顺利举办。会议立足AI时代软件安全、可靠、可信发展需求,围绕科技前沿趋势与未来研究方向开展深度学术对话,共探交叉领域创新发展路径。

本次论坛特别邀请到国际软件工程领域重要奠基者之一——欧洲科学院院士、苏黎世联邦理工学院荣誉退休教授Bertrand Meyer担任主讲嘉宾。作为契约式设计理念开创者,Meyer教授长期深耕软件质量与形式化方法研究,其学术思想对现代软件工程发展进程产生深远影响。会上,Meyer教授围绕软件验证、软件方法论与人工智能融合等前沿方向,分享可信软件构建最新研究成果,深入剖析人工智能应用场景中的机遇与潜在风险。

先进计算方向著名学者杨威教授,浙江大学陈明帅研究员、袁胜浩研究员,华东师范大学软件工程学院(滴水湖国际软件学院)苏亭教授、万成城青年研究员等专家学者也出席论坛并作专题报告。
杨威聚焦大模型驱动的高性能系统软件生成作专题报告,以GPU Kernel优化为例,对比固定流水线与智能体范式两种代码生成方式,探讨AI在系统优化与智能计算基础设施中的应用与未来发展方向。
陈明帅围绕大规模软硬件系统的自动化形式化验证,重点介绍了LLM辅助验证框架PREGUSS,通过融合静态分析与演绎验证,实现真实C程序的近乎全自动验证,并展望了面向更大规模程序验证的智能体扩展方向。

袁胜浩围绕区块链与Rust程序形式化验证展开,介绍了Solana区块链eBPF字节码形式语义研究及Rust验证项目TRust2,展示了形式化验证在基础软件系统安全中的应用价值。

万成城围绕大模型软件集成与质量保障作报告,结合开源LLM应用缺陷分析与运行时框架Comfrey,探讨了AI软件系统中的集成失败问题及自动化防护机制。

苏亭围绕软件自动化功能验证,结合与微信支付合作的自动化验证实践,介绍了模型测试与性质测试结合的方法在保障系统安全与稳定中的作用。

在讨论交流环节,学院师生围绕可信智能、软件验证、AI系统可靠性等前沿议题,与现场多位专家学者展开深入交流。专家学者们结合相关研究方向与实践经验,为青年学子梳理科研思路、指引研究方向、给予专业指导。

研讨会结束后,Bertrand Meyer教授在普陀校区带来专题学术报告《The deal with Design by Contract and why it is worth the fuss》。报告中,他系统阐释了契约式设计这一贯穿软件开发全流程的方法论,深入剖析了其在AI时代实现“构造即正确”可信软件、应对大模型“幻觉”与“直觉式编码”风险的核心价值。

本次系列活动以学科前沿研究为纽带,有效搭建了我院与国内外优质学术资源的交流平台。系列活动不仅帮助师生精准把握行业前沿研究动态、夯实科研基础、拓宽学术研究视野,也进一步深化了学院在可信软件领域的学术积淀。