2025年7月11日，由中国计算机学会（CCF）主办，中国计算机学会（CCF）形式化方法专业委员会和浙江望安科技有限公司联合承办的“‘智领未来’形式化方法产业应用研讨会——中国计算机学会（CCF）形式化方法专业委员会走进望安科技”活动在浙江望安科技有限公司顺利召开。

      中国计算机学会（CCF）形式化方法专业委员会代表、柯桥区委组织部、柯桥区科学技术局、柯桥区大数据发展管理中心、金科桥科技城建设管理委员会、金柯桥数据有限公司、浙江大学形式化研究学者、浙江望安科技有限公司企业代表等约40人参加此次活动，旨在共同探讨形式化方法产业应用的新进展、新机遇和新挑战。

      开幕式上，绍兴金柯桥科技城建设管理委员会张志华主任发表致辞，对莅临的CCF形式化方法专委学者及所有参会者表示热烈欢迎，并介绍了柯桥科技城的基本情况以及本次活动的深远意义，期待本次活动能为望安科技乃至整个区域的科技企业发展提供新的思路和方法。

      CCF形式化方法专委会吴志林秘书长发表致辞，介绍了CCF形式化专委的情况，并向望安科技对本次活动的支持表达谢意，希望此次活动能够增进各位参会人员对形式化方法的了解，促进学术界与产业界的深度融合。

      赵永望教授作《望安科技形式化方法的探索与应用》企业介绍。介绍中提到，望安科技是以“形式化验证”和“安全认证”为核心的安全服务及产品提供商，公司助力中国电子信息产品全面实现“高等级安全”。望安科技依托形式化验证技术，以“形式化验证解决方案”、“安全认证解决方案”为业务主线，致力于为国家重大项目、关键系统及行业企业提供安全保障。公司凭借AI大模型底座，搭建了望安高等级安全SaaS平台，从产品设计/开发阶段的源头到原生安全，到产品运营阶段的国际/国家安全认证背书，实现全生命周期的高等级安全，平台具备原生安全开发工具 W-MetaSec、形式化建模验证工具 W-Cert、全景图 Secinfo、认证工具 W-Caas等，为企业提供一站式安全认证服务。

      在专家报告环节，CCF会士、北京航空航天大学计算机学院博士生导师马殿富教授作《从安全关键软件看复杂软件系统开发与形式验证技术》主题报告，分享了安全关键软件在复杂软件系统开发中的重要性及形式化验证技术的应用。近年来，他主要研究安全关键软件建模、开发与形式验证方法研究，从事基于RISCV的CPU设计与形式证明方法研究、ARINGC653操作系统开发与形式验证方法研究、以及模型语言Lustre及Scade的编译开发与形式证明方法研究。

      北京邮电大学网络空间安全学院博士生导师李晖教授作《密码协议形式化分析技术研究》主题报告，阐述了密码协议及其分析方法，说明使用形式化方法代替人工方法对密码协议进行系统化分析的必要性。她以近年来提出的替代文本密码的登录方式为目标的快速在线认证协议FIDO中的统一认证框架（UAF）和验证OpenSSL协议握手过程的实现是否符合TLS1.3对状态机的要求为例，讲解了密码协议安全性分析及一致性分析的主要思路。

      南京航空航天大学计算机学院博士生导师杨志斌教授作《大模型增强的安全关键软件模型驱动开发与验证方法》主题报告，聚焦大模型增强的模型驱动开发与验证方法，介绍了团队近几年来将大模型技术融入航空航天关键软件模型驱动开发与验证过程的初步探索，主要包括大模型增强的模型驱动安全分析、基于大语言模型的SysML建模、基于大模型的安全关键软件架构建模、基于大模型的时序逻辑公式生成、SCADE模型验证与测试的智能化增强等方面。

      上海海洋大学信息学院硕士生导师，软件工程系副主任张文博教授作《海洋学科距离形式化方法还有多远？》主题报告，详细介绍了上海海洋大学数字海洋研究所近年来在海洋防灾减灾、海洋中尺度现象检测、海冰解译、海底视觉、海洋环境评估、海上风电等方面的研究工作，探讨未来海洋学科与形式化方法深度融合的路径。

      专题报告后，专家们与参会嘉宾开展研讨交流，大家就形式化方法在不同领域的应用前景、技术挑战及未来发展方向等问题进行了深入探讨，现场气氛热烈，思想碰撞不断，研讨会取得圆满成功。