2025年10月29日下午，由华东师范大学软件工程学院（滴水湖国际软件学院）特聘教授刘少英和法国洛林大学计算机科学特级教授Dominique Mery主讲的“高可信软件工程与跨语言形式化方法”学术报告会在普陀校区科学会堂举行，现场气氛热烈。两场报告分别由软件工程学院党委副书记曹桂涛教授和副院长张民教授主持。
报告会现场
刘少英教授报告
刘少英教授在软件工程领域有着深厚的学术造诣和丰富的实践经验，是IEEE Fellow、英国计算机协会BCS Fellow以及AAIA Fellow，已在TSE和ICSE等软件工程领域顶级期刊和会议发表高水平学术论文近百篇。在软件工程领域作为形式化工程方法创始人，成功发起组织软件形式化工程方法国际会议ICFEM，至今已有超20年历史，在软件工程和形式化方法领域形成了较大的学术影响。
刘少英教授在报告中强调，在确保高效率生产的同时保证被开发软件系统的高可信性是软件工程领域亟待解决的重大科学问题。他围绕高可信软件的智能化敏捷形式化工程方法展开了深入讲解，如何把形式化方法有效地融合到软件工程方法和技术中，确立符合软件工程现实特点的敏捷形式化工程方法，以提高软件工程技术的严密性、有效性以及工具的可支撑性。同时，他也提出用人工智能结合编程技术，提供对敏捷形式化工程方法的智能化支持，以提高软件开发过程的高自动化。
Dominique Mery教授报告
Dominique Mery教授是洛林大学南锡学院教授，担任多个国际会议程序委员会成员及主席(如ICFEM、IFM、ABZ、FM等)，是《Formal Aspects of Computing》和《Science of Computer Programming》期刊编委。他的研究聚焦于基于形式化证明的分布式算法开发以及开展医疗器械的建模与认证，主导多项跨语言形式化方法融合项目。
本次报告聚焦Event-B与TLA+两种形式化语言的互补性应用。Mery教授指出，尽管两者均基于集合论、状态不变性等共同概念，但通过跨语言模型转换可显著增强算法正确性验证的可靠性。他详细阐述了从合同到抽象Event-B机器（AEB）、再到最终Event-B机器（FEB）的精化链构建过程，并演示了如何通过Rodin与TLAPM工具链实现顺序算法的自动导出与交叉验证。该研究不仅解决了单一形式化方法在复杂系统验证中的局限性，更通过方法论创新为工业级软件认证提供了可复制的标准化流程。
师生现场互动
在互动环节，现场师生踊跃提问，进行了深入的交流和探讨。两场报告形成了“理论-方法-工具”的完整学术链条，既展现了高可信软件工程从智能化敏捷开发到形式化验证的纵向深化，又体现了国际学术界在跨语言形式化方法上的横向协作。希望本次交流为软件工程发展注入新动能。
