计算机学院高可信与智能化软件研究团队在软件

基础理论与形式化方法领域发表重要研究成果

近日，计算机信息工程学院王昌晶教授带领的高可信与智能化软件研究团队投稿论文“Specification transformation method for functional program generation based on partition-recursion refinement rule”发表在SCI一区TOP期刊Information Sciences, 633 (2023), 613–632上。论文第一作者为左正康博士，合作者为黄箐博士，王昌晶教授为本文的通讯作者，江西师范大学为第一完成单位。

该论文提出了一种基于分区-递归精化规则的函数式程序生成方法，成功给出了一种从规范精化为可执行程序的有效途径。这项工作首次建立了一个基于函数理论的新的程序精化框架，首次将整个程序精化过程视为抽象函数的复合，所得结果是一个函数式可执行程序，特别适用于使用定理证明器如Coq或Isabelle的自动证明。为了验证所提方法的有效性，首次对多项式乘法进行了变换。结果表明，该方法可以大幅度简化转换步骤，减少生成代码的行数，在数值类问题上取得了很好的实验结果。

该文是江西省软件基础理论与形式化方法领域首次在SCI一区发文，为学校软件工程博士点申报提供了支持。

论文链接： https://authors.elsevier.com/a/1gnWf4ZQEBs1P。

作者简介：

左正康，博士，副教授，硕士生导师，毕业于中国科学院软件研究所，师从“国家有突出贡献中青年专家”、“国家杰出青年基金会评专家”薛锦云教授。主持完成 2项国家自然科学基金地区科学基金项目，主持立项1项国家留学基金面上项目。在国内外高水平学术期刊和会议上发表了 40余篇论文，包括《IEEE Transactions on Services Computing》、《Information Sciences》、《Cluster Computing》、《International Journal of Software Engineering and Knowledge Engineering》、《软件学报》、《电子学报》、《计算机研究与发展》、《信息安全学报》、《武汉大学学报（自然科学英文版）》、ICECCS、QRS、ICFEM、FAW等。出版了一本学术专著（科学出版社），并获授权一项国家发明专利。目前是 CCF形式化方法专委会和理论计算机科学专委会的执行委员，同时也是 CCF高级会员。多次受邀在国际国内重要学术会议上做学术报告，包括 ICECCS、QRS、CCF中国软件大会 ChinaSoft和全国理论计算机科学学术年会等，受邀担任2021年全国理论计算机科学学术年会分论坛主席，以及 2020年和 2021年全国理论计算机科学学术年会的程序委员会委员。

王昌晶，博士，教授，博士生导师，毕业于中国科学院软件研究所，师从薛锦云教授。主要从事高可信软件与智能化软件工程的研究。近年来，在国内外学术刊物上发表论文60余篇，含ICSE 2023、TSC、软件学报、电子学报、计算机研究与发展等重要学术刊物，其中40余篇被SCI/EI检索。主持国家课题2项，主持省部级课题9项，含重点课题3项。获2016年度中国精品科技期刊顶尖学术论文奖。CCF高级会员，理论计算机科学专委、形式化方法专委执行委员。国家自然科学基金评审专家、科技部国家科技专家库专家、江西省科技奖励评审会评专家。曾赴澳大利亚、美国、英国做访问学者。

黄箐，博士，副教授，硕士生导师，毕业于武汉大学计算机学院，主要从事智能化软件工程的研究。系我校计算机信息工程学院于2018年引进的优秀博士。入校以来，黄箐博士以第一作者身份发表包括ASE 2022、ICSE 2023、ASE、SANER、SPE、SCIS、IS等CCF推荐A/B论文10余篇。主持国家自然科学青年基金1项，国家自然科学地区基金1项，国家留学基金委面上项目1项，江西省自然科学基金面上项目1项。