AI 中文总结
本文提出CPV框架，将C程序转时序电路并调用硬件模型检查器，在16000+任务基准上验证，其性能与成熟软件验证器相当且可解决其他工具无法处理的任务。
AI 中文摘要
软件程序与硬件设计的形式化验证有着共同的目标，即对状态转换系统进行推理，但两个领域在很大程度上开发了各自独立的中间表示和验证算法。本文研究将时序电路用作软件验证的中间表示，目标是实现硬件模型检查技术的直接应用。我们提出了基于电路的程序验证（Circuit-Based Program Verification, CPV），这是一个模块化框架，可将C程序转换为时序电路，并采用现成的硬件模型检查器作为后端。与通常依赖基于路径的探索的传统软件验证器不同，CPV 对时序电路进行推理，其中程序的控制流和数据流被整合为一个整体转换关系，可作为一个整体进行分析。该框架支持可达性安全性和终止性分析，并集成了多个最先进的硬件模型检查器，这些检查器共同提供了多种验证算法，包括有界模型检查、k-归纳和 IC3/PDR。硬件模型检查器发现的反例会自动转换回软件验证见证，供用户解释验证结果。我们对包含超过16000个任务的基准套件进行了综合评估，结果显示，CPV 与五个成熟的软件验证器相比表现出竞争力，且具有互补优势，能独力解决其他验证器无法处理的任务。
英文摘要
Formal verification of software programs and hardware designs shares the common goal of reasoning about state-transition systems, yet the two communities have largely developed separate intermediate representations and verification algorithms. This paper investigates sequential circuits as an intermediate representation for software verification, with the goal of enabling direct application of hardware-model-checking techniques. We present Circuit-Based Program Verification (CPV), a modular framework that translates C programs into sequential circuits and employs off-the-shelf hardware model checkers as backends. Unlike traditional software verifiers, which typically rely on path-based exploration, CPV reasons over sequential circuits, where a program's control and data flows are folded into a monolithic transition relation that can be analyzed as a whole. The framework supports reachability-safety and termination analyses and integrates multiple state-of-the-art hardware model checkers, which together provide access to diverse verification algorithms, including bounded model checking, $k$-induction, and IC3/PDR. Counterexamples found by hardware model checkers are automatically translated back into software-verification witnesses for users to interpret verification results. We conducted a comprehensive evaluation on a benchmark suite of more than 16000 tasks. Our results show that CPV achieved competitive performance against five well-established software verifiers and exhibited complementary strengths by uniquely solving tasks that other verifiers cannot handle.
