2022CCF中国软件大会形式化方法工
11月27日，年CCF中国软件大会“形式化方法工业应用前沿”技术分论坛于线上顺利召开。本次活动由CCF形式化方法专业委员会主办，华东师范大学、国防科技大学承办，上海工业控制安全创新科技有限公司、科大国创软件股份有限公司、安徽中科国创高可信软件有限公司协办。活动邀请工业界与学术界的顶尖专家，聚焦工业领域中形式化方法的应用探索，共同讨论形式化方法在工业领域应用的最佳实践以及发展趋势。活动于腾讯会议等多个平台同步直播，受到业界同行及高校师生的热烈响应，超1,人次实时在线观看。会上，同步举办中科国创高可信与上海控安新品联合发布会。
活动由华东师范大学软件工程学院执行院长、教授、博士生导师、上海控安总经理蒲戈光，国防科技大学计算机学院教授、博士生导师董威担任主席。蒲戈光作开场致辞，介绍本次论坛的背景与意义。他表示形式化方法是保障软硬件可靠性与正确性的重要手段，目前已覆盖芯片验证、操作系统验证、程序分析等工业应用领域。本次活动希望通过工业界与学术界的交流，共同促进形式化方法领域产业与学术共同体的发展。董威向莅临参会的各位嘉宾表示欢迎，并担任本次论坛主持。
国防科技大学计算机学院董威报告分享
随后，来自科大国创高可信公司、华东师范大学、华为、芯华章科技股份有限公司等优秀企业高校的多位专家学者作主题报告演讲。
科大国创高可信公司，研发总监，李兆鹏，以“形式化方法在工业控制领域的研究与实践”为主题，结合自身实战经验，着重讨论当下形式化方法的程序验证实践与静态分析实践，并展望工业领域中形式化方法的发展与挑战。
科大国创高可信公司李兆鹏华东师范大学软件工程学院，教授、博士生导师，李建文，围绕“形式化验证技术及其EDA应用案例”，介绍当前主流硬件形式化验证技术的基本原理、发展进程和现有不足，并通过实践案例阐述理论研究与实际应用场景相结合的具体途径。
华东师范大学软件工程学院李建文华为操作系统内核实验室，工程师，李屹，就“操作系统开发中的形式化验证：挑战与思考”进行演讲，结合自身在操作系统内核形式化验证方面的实践经验，分享在形式化验证实践过程中所遇到的挑战，以及相应的解决措施与思考。
华为操作系统内核实验室李屹华为公司可信系统工程实验室，技术专家，梁智章，分享主题“安全攸关领域的形式化方法试点和探索”，介绍形式化方法在安全攸关领域中的落地应用，并分享华为可信系统工程实验室对形式化方法的应用和探索。
华为公司可信系统工程实验室梁智章芯华章科技动态仿真与形式验证部，研发总监，刘军，围绕主题“形式验证覆盖率分析加速芯片验证收敛”，以芯片验证领域中的形式化方法发展进程为切入点，分享形式验证的具体实践与思考。
芯华章科技动态仿真与形式验证部刘军产品发布
活动最后，中科国创高可信与上海控安联合发布形式化软件工具链——“科创星云验证器（企业版）”“SmartRocketModeler可视化建模开发工具（beta版）”。中科国创高可信市场总监李超钰、咨询总监周洋，上海控安产品总监包丹珠，以及线上各位嘉宾观众共同见证产品发布。李超钰表示，本次联合发布的形式化软件工具链将形式化技术应用于实践，推动了形式化方法的深化与创新，为关键行业领域的数智化产品进一步提供了保障与支撑，也为中国乃至全球的工业软件安全保障提供了多种可能性。
产品发布中科国创高可信科创星云验证器（企业版），采用自主设计的安全C规范语言作为规约语言，对程序的行为进行形式化描述。基于Hoare逻辑，采用最强后条件的演绎推理技术，将程序满足其形式规约的证明问题转化为一组数学命题的证明，并实现程序验证的自动化。科创星云验证器主要用于关键核心代码的验证，比如操作系统内核、数据库引擎、关键的嵌入式软件等，为航空航天、汽车电子、能源核电、轨道交通等安全攸关领域的高可信软件开发提供安全保障。
科创星云验证器（企业版）
转载请注明：http://www.abuoumao.com/hykh/5946.html
