Software Foundations Series
6 hours ago
- 《软件基础》系列为可靠软件的数学基础提供了广泛的介绍。
- 该系列中的每一个细节都使用Rocq证明助手进行了完全形式化和机器验证。
- 该系列面向从高年级本科生到研究人员的广泛受众，假定没有先前的逻辑或编程语言背景。
- 第一卷（逻辑基础）涵盖函数式编程、逻辑基础和Coq定理证明。
- 第二卷（编程语言基础）涵盖操作语义、霍尔逻辑和静态类型系统。
- 第三卷（验证的函数式算法）专注于规范并机械验证基本数据结构。
- 第四卷（QuickChick）介绍结合Coq形式规范的基于属性的测试。
- 第五卷（可验证C语言）提供使用普林斯顿验证软件工具链验证实际C程序的实践教程。