导语
形式化方法是具有严格数学基础的保障计算机软硬件正确性与安全性的方法，在近20年取得了长足进步，已经在国内外头部公司（比如微软、亚马逊、华为等）取得了成功应用。
形式化方法经过几十年已经发展出了多种技术，包括约束求解、模型检测、定理证明、抽象解释等。形式化方法的应用领域也不断扩展，包括芯片设计验证、操作系统验证、编译器验证、网络验证、区块链智能合约验证、数据库查询等价性验证、智能系统验证等。而且近年来，形式化方法作为人工智能符号学派的代表，如何和以深度学习为代表的人工智能统计学派进行交叉融合，已经成为研究热点和难点。
01
孙军教你用抽象解释解决非线性问题
线性方程简单易解，但遇到非线性的怎么办？孙军教你用抽象解释将复杂问题简化为线性，轻松解决！
扫码观看视频内容
02
孙猛详解CKB性能突破
【点击观看】
孙猛详细讲解CKB共制协议如何通过两步确认机制与动态难度调整，有效减少无效操作并提供奖励
扫码观看视频内容
03
翟恩南揭秘资源优化新方法
通过编译技术实现资源的高效利用，翟恩南带你了解资源优化新方法
扫码观看视频内容
04
汪宇霆带你破解编程难题
如何将局部变量合并成一个整体？汪宇霆教你调整这些关键参数
扫码观看视频内容
05
李屹揭秘用C语言验证操作系统链表的合法性
李屹探索如何使用C语言编写的操作系统内核，并通过定理证明器进行形式化验证。了解如何确保链表的合法性和数据指针的有效性
扫码观看视频内容
更多精彩尽在Link APP
关于栏目
《CCF 大咖60秒》是CCF 推出的硬核知识视频栏目，内容选自CCF各类精彩活动、数字图书馆编委会，以“60秒速递”的形式传递讲者观点，共享知识普及。
往期回顾
点击“阅读原文”，查看详情。
