面向形式化证明的程序设计语言
以下摘要由 AI 根据胶片自动生成。
形式化证明软件（如 seL4 微内核）成本极高，且须分别掌握 C、Haskell、 Isabelle/HOL 等多套工具，开发门槛严重制约了高安全软件的普及。本报告提出 C*——一种在同一语言中统一编写功能代码、规约代码与证明代码的类 C 编程语言，采用 LCF 证明核心并支持命令式风格的后向证明与 SMT 自动证明。短期原型基于 VST-A 框架实现，将带标注的 C 程序通过符号执行与 Coq 中的分离逻辑验证环境无缝衔接。
以下摘要由 AI 根据胶片自动生成。
形式化证明软件（如 seL4 微内核）成本极高，且须分别掌握 C、Haskell、 Isabelle/HOL 等多套工具，开发门槛严重制约了高安全软件的普及。本报告提出 C*——一种在同一语言中统一编写功能代码、规约代码与证明代码的类 C 编程语言，采用 LCF 证明核心并支持命令式风格的后向证明与 SMT 自动证明。短期原型基于 VST-A 框架实现，将带标注的 C 程序通过符号执行与 Coq 中的分离逻辑验证环境无缝衔接。