C*：统一 C 语言编程和验证

计算机科学 > 编程语言 arXiv:2504.02246 (cs) [提交于 2025 年 4 月 3 日] 标题：C*：统一 C 语言编程与验证 作者：Yiyuan Cao、Jiayi Zhuang、Houjin Chen、Jinkai Fan、Wenbo Xu、Zhiyi Wang、Di Wang、Qinxiang Cao、Yingfei Xiong、Haiyan Zhao、Zhenjian Hu 查看论文的 PDF题为《C*：用 C 语言统一编程和验证》，作者：Yiyuan Cao 和其他 10 位作者 查看 PDF HTML（实验） 摘要：鉴于系统软件的安全关键性和低级性质，确保系统软件的正确功能是形式验证研究和应用的主要焦点。尽管验证工具取得了进步，但传统程序员很少参与自己代码的验证，导致经过验证的软件的开发和维护成本更高。程序员参与验证实践的一个关键障碍是编程和验证实践之间的环境和范式脱节，这限制了可访问性和实时验证。我们介绍 C*，一种用于 C 编程的证明集成语言设计。 C* 扩展了 C 的验证功能，由符号执行引擎和 LCF 风格的证明内核提供支持。它允许程序员将证明代码块与实现代码一起嵌入，从而实现实时验证，从而促进对当前证明状态的交互式更新。其富有表现力和可扩展的证明支持允许用户构建可重用的逻辑定义、定理和可编程证明自动化库。至关重要的是，C* 通过使用 C 作为通用语言来统一实现和验证代码开发。我们实现了 C* 的原型，并在小型 C 程序的代表性基准和具有挑战性的现实案例研究上对其进行了评估：pKVM 的伙伴分配器的附加功能。我们的结果表明，C* 支持对 C 编程习惯的广泛子集进行验证，并有效处理现实场景中的复杂推理任务。科目：编程语言（cs.PL）；软件工程 (cs.SE) 引用为：arXiv:2504.02246 [cs.PL]（或本版本的 arXiv:2504.02246v1 [cs.PL]） https://doi.org/10.48550/arXiv.2504.02246 重点了解更多 arXiv 通过 DataCite 发布的 DOI 提交历史 来自：Yiyuan Cao [ 查看电子邮件 ] [v1] 2025 年 4 月 3 日星期四 03:22:22 UTC (414 KB) 全文链接： Access Paper：查看由 Yiyuan Cao 和其他 10 位作者撰写的标题为 C*：统一 C 语言编程和验证的论文的 PDF 查看 PDF HTML（实验性）TeX 源代码 查看许可证 当前浏览上下文：cs.PL < prev |下一页 > 新 |最近 | 2025-04 更改为浏览方式：cs cs.SE 参考文献与引文 NASA ADS Google Scholar 语义学者导出 BibTeX 引文 正在加载... BibTeX 格式的引文 × 正在加载... 数据提供者： 书签 书目工具 书目和引文工具 书目浏览器 切换书目浏览器（什么是浏览器？） 已连接论文 切换已连接论文（什么是已连接）论文？ ) Litmaps 切换 Litmaps（什么是 Litmaps？） scite.ai 切换 scite 智能引文（什么是智能引文？） 与本文相关的代码、数据、媒体 代码、数据和媒体 alphaXiv 切换 alphaXiv（什么是 alphaXiv？） 代码链接 切换 CatalyzeX 论文代码查找器（什么是 CatalyzeX？） DagsHub 切换 DagsHub (什么是 DagsHub？) GotitPub 切换 Gotit.pub (什么是 GotitPub？) Huggingface 切换拥抱面 (什么是 Huggingface？) ScienceCast 切换 ScienceCast (什么是 ScienceCast？) 演示 演示 复制 切换复制 (什么是复制？) Spaces 切换拥抱面 空间 (什么是空间？ ) 空间 切换 TXYZ.AI（什么是 TXYZ.AI？） 相关论文推荐器和搜索工具 链接到 Influence Flower Influence Flower（什么是 Influence Flowers？） 核心推荐器切换 CORE 推荐器（什么是 CORE？） 作者地点 机构 主题 关于 arXivLabs arXivLabs：与社区合作者的实验项目 arXivLabs 是一个允许合作者开发和共享新 arXiv 的框架直接在我们的网站上提供功能。与 arXivLabs 合作的个人和组织都接受并接受了我们开放、社区、卓越和用户数据隐私的价值观。 arXiv 致力于这些价值观，并且只与遵守这些价值观的合作伙伴合作。您有一个能为 arXiv 社区增加价值的项目想法吗？了解有关 arXivLabs 的更多信息。这篇论文的哪些作者是认可者？ |禁用 MathJax（什么是 MathJax？）