首页

首页

【创源大讲堂】软件系统全生命周期形式化的理论与方法

来源:计算机与人工智能学院 日期:2026/06/09 作者:邹远 责编:冉孟雨

讲座时间:2026年06月11日(星期四)下午15:00

讲座地点:犀浦校区3号教学楼X31541报告厅

主讲人:蒋建民 教授

主讲人简介

蒋建民,成都信息工程大学教授,CCF理论计算机科学、系统软件专委会委员。四川省创新领军人才,四川省特聘专家。2023年、2024年入选美国斯坦福大学和爱思唯尔数据库发布全球2%顶尖科学家榜单。主要从事软件开发方法、形式化方法研究,主持国家重点研发项目课题、国家自然科学基金等项目。以第一作者在国际权威刊物Information and Computation、ACM TOSEM、ACM TECS、ACM TMIS、ACM TCPS和国内中国科学—信息科学(英文版)等学术期刊发表论文40余篇。

内容简介

现有形式化方法多采用单一视点(行为方面)和单一形式化模型(语言)进行建模与分析,在实际软件开发过程中往往仅作为补充手段引入,未能与非形式化开发方法实现有机融合。大语言模型能高效地生成程序代码,但无法完全保证它们的正确性。为此,探索在基于大语言模型辅助下将形式化方法深度融入软件全生命周期的理论和方法,包括:(1)提出了一种新的形式化模型,支持多视点、多层次的推理;(2)利用新模型表示多种非形式化或半形式化模型,并借助大语言模型和自动化工具,实现从可视化模型(如UML)到新形式化模型的自动转换,从而降低工程师的学习成本;(3)研究了全自动程序代码生成的前提条件,并验证基于大语言模型自动生成代码的正确性。我们的研究希望建立一套既能发挥大语言模型高效性、又能保证软件系统正确性的新型软件开发范式。