形式验证：基础工具与前沿挑战 CCF形式化方法专委会战略研讨暨2023年第1期前瞻科技智库论坛

https://www.chaspark.com/#/live/885610496333578240
视频笔记（飞书妙记字幕待传）：https://www.notion.so/eatcosmos/CCF-2023-1-159f0042a73c4d0a8b192b8523509b4f?pvs=4

计算系统包括软件、硬件和网络，是现在信息技术的基石。随着人机物融合计算范式的发展，计算系统与人们日常生活更加紧密，而且很多计算系统都是安全攸关或者使命攸关（例如在航空航天、核电、国防等关键领域），因此对这些系统的可信性要求越来越高。然而，计算机系统功能越来越强大的同时，系统结构变得越来越复杂，软件定义一切的新趋势使得计算机系统中软件比重越来越大，软硬协同使得软件和硬件深度耦合，开发可信的计算系统变得越来越困难。

形式化方法基于严格数学，为设计、分析和验证计算系统提供规约、分析、验证和构造理论、方法和技术。形式化方法是设计和验证可信计算系统的一种重要途径，已经成为各种安全攸关系统设计开发国际和行业标准的必备关键技术。美国自然基金会实施了“形式化方法在不同领域”（Formal Methods in the Field，FMitF）的重大研究计划 。

本次战略研讨会将邀请国内形式化方法、编程语言等相关方向的专家学者围绕形式验证基础工具与前沿挑战进行研讨，比较中外发展差距，讨论未来发展趋势及我国应对策略，凝练形式化方法和编程语言领域的重点研究方向，为国家计算机软件与理论学科重点项目布局规划提供建议和参考。