“形式化工程数学”的研究方向——CCF第三期启智会在苏州举行

2017年9月6日-8日，中国计算机学会（CCF）第三期启智会在苏州金鸡湖举行。会议由首都师范大学教授施智平和航天科工三院304所国家千人计划专家陈钢召集，北京大学教授裘宗燕和波特兰州立大学教授宋晓宇主持，还聚集了来自北京航空航天大学、南京航空航天大学、清华大学、航天二院、中科院软件所、苏州新火花公司等多家单位的形式化方法和工程科学方向的共计16位专家学者。

本次研讨的主要目的是提出“形式化工程数学”这一学术研究方向，同时也讨论形式化方法在工程科学中的应用，推动各个工程领域的形式化工程数学的规模化开发工作。“形式化工程数学”的一个重要特点是同工程系统设计和工程软件的开发有紧密联系。因此，会上也讨论了形式化方法在工程软件开发中的应用问题，以及形式化工程数学同其他形式化方法的关联发展问题。

形式化数学是30多年前国际上一批理论计算机科学家和数学家共同提出的一个概念，其总体目标是在定理证明器中实现所有数学理论的形式化，包括定义数学概念，验证数学定理的证明，构造形式化数学知识库。这一概念的提出引导和促进了各个数学分支的形式化发展。在各个工程科学领域中，虽然也存在着大量的数学推导和数学理论，但是目前只有零星的形式化工作，并没有形成规模化的形式化工程数学库的开发工作。航天科工和企业界专家指出形式化方法在工程数学推导验证以及工程软件开发中具有很大的应用潜力，工程数学的软件实现在整个工程软件中占有非常重要的地位。与专家们也认为建设形式化工程数学库，并在此基础上开发经过形式验证的软件库，对于工程软件的发展具有重要意义。

本次研讨会采用短报告和讨论相互交替的方式进行。每个短报告均以一个特定角度讨论形式化工程数学的一个主要方面，带动相关问题的提出和讨论。具体研讨的议题包括：形式化工程数学的重要性、内容、前景、技术难点、同相关学科关系、形式化数学库开发、数学软件库的形式化开发，以及怎样在这些库的基础上支持工程软件开发及形式验证、国内外发展状况、如何争取社会支持等方面问题。

与会专家一致认为CCF启智会这种非正式学术的会议形式新颖，一方面有助于科研人员能够去思考有长远影响的科技方向问题，另一方面也促进了新思想的产生和碰撞。

会议合影（由左至右）：陈钢 高坚强 胡凯 康烁 刘嘉祥 马殿富 裘宗燕 施智平 施晓牧 宋晓宇 赵永望 

                         詹乃军 杨志斌 王泊涵 王国辉 王生原

会议现场