作者Yiyuan Cao、Jiayi Zhuang、Houjin Chen、Jinkai Fan、Wenbo Xu、Zhiyi Wang、Di Wang、Qinxiang Cao、Yingfei Xiong、Haiyan Zhao和Zhenjiang Hu介绍了C*，这是一种面向C语言编程的证明集成语言设计。C*通过符号执行引擎和LCF风格的证明内核，为C语言扩展了验证能力。它通过允许程序员在实现代码旁嵌入证明代码块，实现实时验证，便于交互式更新当前证明状态。其富有表现力且可扩展的证明支持，允许用户构建逻辑定义、定理和可编程证明自动化的可复用库。关键在于，C*通过使用C作为通用语言，统一了实现代码与证明代码的开发。团队实现了一个原型，并在具有代表性的小型C程序基准测试和一个具有挑战性的真实案例研究——p KVM伙伴分配器的attach函数——上进行了评估。结果表明，C*支持广泛C语言编程习语的验证，并能有效处理真实场景中的复杂推理任务。