CCF形式化专委走进望安 | “智领未来”形式化方法产业应用研讨会

   张志华，绍兴金柯桥科技城建设管理委员会主任、党工委副书记；绍兴柯桥经济技术开发区党工委副书记

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

    吴志林，中国计算机学会形式化方法专委会秘书长；

中国科学院软件研究所研究员/博导

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

赵永望，望安科技创始人，董事长；浙江大学教授，博士生导师

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

马殿富，北京航空航天大学计算机学院教授，中国计算机学会会士、监事

        马殿富教授作《从安全关键软件看复杂软件系统开发与形式验证技术》主题报告，分享了安全关键软件在复杂软件系统开发中的重要性及形式化验证技术的应用。近年来，主要研究安全关键软件建模、开发与形式验证方法研究，从事基于RISCV的CPU设计与形式证明方法研究、ARINGC653操作系统开发与形式验证方法研究、以及模型语言Lustre及Scade的编译开发与形式证明方法研究。

李晖，北京邮电大学网络空间安全学院教授，博士生导师

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

杨志斌，南京航空航天大学计算机学院教授，博士生导师

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

张文博，上海海洋大学信息学院副教授，软件工程系副主任

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

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

    本次研讨会的成功举办，不仅为形式化方法领域的专家学者提供了深度交流平台，也为望安科技发展提供了新思路、新方向。未来，望安科技期待与各界合作伙伴携手共进，共同推动形式化方法在实际产业中的深度应用。