Wirth's Revenge 编译器架构：形式化验证与语义正确性的复兴之路
分析 Wirth 精简编译器设计哲学如何天然契合形式化验证需求，并探讨 CompCert 等验证性编译器如何通过语义保持证明对抗软件膨胀带来的不可靠性。
阅读全文 →
←所有分类
compilers-formal-verification
技术与实践
Zirgen DSL类型系统与形式化验证集成：类型推导算法与定理证明器接口设计
面向零知识证明算术电路编译器Zirgen，设计类型系统与形式化验证工具的集成架构，提出类型推导算法与定理证明器接口的具体实现方案。
阅读全文 →