11月27日，2022年CCF中国软件大会“形式化方法工业应用前沿”技术分论坛暨中科国创高可信联合上海控安新品发布会于线上顺利召开。本次活动由CCF形式化方法专业委员会主办，华东师范大学、国防科技大学承办，上海工业控制安全创新科技有限公司、科大国创软件股份有限公司、安徽中科国创高可信软件有限公司协办，邀请到工业界与学术界的顶尖专家，聚焦工业领域中形式化方法的落地实践，共同讨论形式化方法在工业应用领域的现状与趋势。活动于腾讯会议等多个平台同步直播，受到业界同行及高校师生的热烈响应，超1,000人次实时在线观看。

活动由华东师范大学软件工程学院执行院长、教授、博士生导师、上海控安总经理蒲戈光，国防科技大学计算机学院教授、博士生导师董威担任主席。蒲戈光作开场致辞，介绍本次论坛的背景与意义。他表示形式化方法是保障软硬件可靠性与正确性的重要手段，目前已覆盖芯片验证、操作系统验证、程序分析等应用领域。本次活动希望通过工业界与学术界的交流，共同促进形式化方法领域产业与学术共同体的发展。董威主持本次活动，并向莅临参会的各位嘉宾表示欢迎，同时预祝活动圆满完成。

'

▲ 国防科技大学计算机学院 董威

随后，来自科大国创高可信公司、华东师范大学、华为、芯华章科技股份有限公司等优秀企业高校的多位专家学者作主题报告演讲。

科大国创高可信公司，研发总监，李兆鹏，以“形式化方法在工业控制领域的研究与实践”为主题，结合自身实战经验，着重讨论当下形式化方法的程序验证实践与静态分析实践，并展望工业领域中形式化方法的发展与挑战。

'

▲ 科大国创高可信公司 李兆鹏

华东师范大学软件工程学院，教授、博士生导师，李建文，围绕“形式化验证技术及其EDA应用案例”，介绍当前主流硬件形式化验证技术的基本原理、发展进程和现有不足，并通过实践案例阐述理论研究与实际应用场景相结合的具体途径。

'

▲华东师范大学软件工程学院 李建文

华为操作系统内核实验室，工程师，李屹，就“操作系统开发中的形式化验证：挑战与思考”进行演讲，结合自身在操作系统内核形式化验证方面的实践经验，分享在形式化验证实践过程中所遇到的挑战，以及相应的解决措施与思考。

'

▲ 华为操作系统内核实验室 李屹

华为公司可信系统工程实验室，技术专家，梁智章，分享主题“安全攸关领域的形式化方法试点和探索”，介绍形式化方法在安全攸关领域中的落地应用，并分享华为可信系统工程实验室对形式化方法的应用和探索。

'

▲ 华为公司可信系统工程实验室 梁智章

芯华章科技动态仿真与形式验证部，研发总监，刘军，围绕主题“形式验证覆盖率分析加速芯片验证收敛”，以芯片验证领域中的形式化方法发展进程为切入点，分享形式验证的具体实践与思考。

'

▲ 芯华章科技动态仿真与形式验证部 刘军

活动期间，中科国创高可信与上海控安联合发布形式化软件工具链——“科创星云验证器（企业版）”& “SmartRocket Modeler可视化建模开发工具（beta版）”。中科国创高可信市场总监李超钰、咨询总监周洋，上海控安产品总监包丹珠，以及线上各位嘉宾观众共同见证产品发布。李超钰表示，本次联合发布的形式化软件工具链将形式化技术应用于实践，推动了形式化方法的深化与创新，为关键行业领域的数智化产品进一步提供了保障与支撑，也为中国乃至世界的软件安全保障提供了多种可能性。

'

▲ 产品发布

中科国创高可信 科创星云验证器（企业版），采用自主设计的安全C规范语言作为规约语言，对程序的行为进行形式化描述。基于Hoare逻辑，采用最强后条件的演绎推理技术，将程序满足其形式规约的证明问题转化为一组数学命题的证明，并实现程序验证的自动化。科创星云验证器主要用于关键核心代码的验证，比如操作系统内核、数据库引擎、关键的嵌入式软件等，为航空航天、汽车电子、能源核电、轨道交通等安全攸关领域的高可信软件开发提供安全保障。

'

▲ 科创星云验证器（企业版）

官网：www.ustchcs.com

邮箱：info@ustchcs.com

电话：0551-65396781

上海控安 SmartRocket Modeler可视化建模开发工具，是一款国产自主可控的可视化建模开发工具。该工具支持嵌入式软件模型的设计与开发，能够从系统需求出发，为用户提供基于Lustre模型语言的图形化建模、模型静态检查、模型仿真与调试、模型在环测试、C代码自动生成等丰富便捷的功能。同时工具也支持全系列国产操作系统，为国内高端制造领域的嵌入式软件研制提供支撑平台，为逐步摆脱对国外同类软件的依赖提供有效解决方案。

'

▲ SmartRocket Modeler可视化建模开发工具（beta版）

官网：www.ticpsh.com

邮箱：Marketing@ticpsh.com

电话：021-62655886

（工作日09:00-18:00）

至此，2022 CCF形式化方法工业应用前沿分论坛圆满完成。活动期间，专家学者通过视频分享精彩观点，并与线上与会的嘉宾积极互动，从工业界与学术界等维度热烈探讨形式化方法的具体落地实践，共同促进形式化方法的理论研究、工具成果和行业实践的融合发展。