AI 中文总结
研究如何将C程序验证任务编码为BTOR2模型，提出C2Btor方法，该方法用程序计数器等进行相关表示与映射。通过在基准测试上与其他工具比较，C2Btor解决任务更多，尤其在比特向量基准测试上效果好，让C程序验证受益于硬件模型检查后端进展。
AI 中文摘要
程序验证工具常依赖特定中间表示和分析后端，限制了验证算法和模型检查器在框架间的复用。硬件模型检查有成熟后端生态系统，如BTOR2支持反例搜索和归纳安全证明的可复用算法。本文提出C2Btor方法，将验证任务编码为BTOR2模型，用程序计数器捕获控制转移等。在SV-COMP C ReachSafety基准测试等上评估，C2Btor比CBMC多解决101个任务，在比特向量基准测试上效果尤佳。结果表明BTOR2路线使C程序验证受益于硬件模型检查后端进展。
英文摘要
Program verification tools often rely on specific intermediate representations and analysis backends, limiting the reuse of verification algorithms and model checkers across frameworks. In contrast, hardware model checking has developed a mature backend ecosystem, where standard formats such as BTOR2 support reusable algorithms for counterexample search and inductive safety proving. Applying these capabilities to C requires translating assertion-based programs into transition systems that hardware model checkers can directly process. We present C2Btor, a method for encoding such verification tasks into BTOR2 models. C2Btor uses a program counter to capture control transfers, represents data states and memory objects with bit-vectors and arrays, and maps assumptions and assertion checks into BTOR2 constraints and bad-state properties. We evaluate C2Btor on SV-COMP C ReachSafety benchmarks and a curated assertion-category benchmark suite, comparing it with representative program verification tools. C2Btor correctly solves 263 tasks, 101 more than CBMC configured with bounded model checking, and is especially effective on bit-vector benchmarks, where it solves 75.5% of the tasks with no wrong verdicts. These results show that the BTOR2 route allows C program verification to benefit from advances in hardware model-checking backends, expanding the available capability for counterexample search, inductive safety proving, and word-level transition-system reasoning.
Comments12 pages, 3 figures
