C*：用 C 语言本身统一编程与形式化验证

📋 概述

论文提出 C*——一种面向 C 编程的“证明融入式”语言设计，试图降低系统软件形式化验证的门槛。现状是验证工具虽不断进步，但常规程序员很少参与自己代码的验证，根源在于编程与验证的范式和环境彼此割裂。C* 以 C 为共同语言，把验证能力直接扩展进 C：内置符号执行引擎与 LCF 风格证明内核，允许程序员在实现代码旁嵌入证明代码块，实时交互地更新当前证明状态；其表达力强、可扩展的证明支持还能沉淀可复用的逻辑定义、定理与可编程证明自动化库。作者在小型 C 程序基准与 pKVM buddy 分配器的 attach 函数这一真实案例上做了验证。