BTOR2-Based C Program Verification via Hardware Model Checking
2026-07-20 • Software Engineering
Software EngineeringFormal Languages and Automata Theory
AI summaryⓘ
The authors present C2Btor, a tool that converts C programs with assertions into a format (BTOR2) widely used in hardware model checking. This allows existing powerful hardware verification tools to check C programs by representing program states and memory as bit-vectors and arrays. Their tests show C2Btor performs better than some current software verification tools, especially on tasks involving bit-level data. This approach bridges software and hardware verification techniques, enabling improved analysis of C programs using established hardware model-checking methods.
Program verificationIntermediate representationModel checkingBTOR2 formatTransition systemsBit-vectorsBounded model checkingAssertion verificationHardware model checking
Authors
Xinyu Zhang, Runxuan Fang, Ziqun Bao, Yechuan Xia, Jianwen Li, Geguang Pu
Abstract
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.