形式化方法赋能计算机其他领域|CCF数图焦点第39期

编者寄语

形式化方法是具有严格数学基础的保障计算机软硬件正确性与安全性的方法，在近20年取得了长足进步，已经在国内外头部公司（比如微软、亚马逊、华为等）取得了成功应用。

形式化方法经过几十年已经发展出了多种技术，包括约束求解、模型检测、定理证明、抽象解释等。形式化方法的应用领域也不断扩展，包括芯片设计验证、操作系统验证、编译器验证、网络验证、区块链智能合约验证、数据库查询等价性验证、智能系统验证等。而且近年来，形式化方法作为人工智能符号学派的代表，如何和以深度学习为代表的人工智能统计学派进行交叉融合，已经成为研究热点和难点。

本次专题聚焦形式化方法赋能计算机其他领域，将CCF数字图书馆相关报告视频和期刊文章资源以及其他平台与选题相关的资源进行聚合，方便会员集中观看学习，也为读者探索形式化方法与计算机其他领域的交叉融合抛砖引玉。

目录