BTOR2-Based C Program Verification via Hardware Model Checking

• URL: http://arxiv.org/abs/2607.17622v1
• Date: Mon, 20 Jul 2026 07:18:59 GMT
• Title: BTOR2-Based C Program Verification via Hardware Model Checking
• Abstract summary: We present C2Btor, a method for encoding verification tasks into BTOR2 models.<n>C2Btor correctly solves 263 tasks, 101 more than CBMC configured with bounded model checking.
• Score: 10.596871975682978
• License: http://creativecommons.org/licenses/by-nc-nd/4.0/
• 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.

Related papers

• Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST [32.505127447635864]
  We report on the verification of memory safety for decoder components of liblzma.<n>The verification exposed undefined behavior in raw LZMA1 zero-input handling.<n>Unlike similar work that synthesizes verified code, we verify pre-existing, production-scale C.
  arXiv  Detail & Related papers  (2026-08-30T10:50:56Z)
• Circuit-Based Program Verification: Sequential Circuits as an Intermediate Representation for Verifying C Programs [5.82728420508304]
  This paper investigates sequential circuits as an intermediate representation for software verification.<n>We present Circuit-Based Program Verification (CPV), a modular framework that translates C programs into sequential circuits.
  arXiv  Detail & Related papers  (2026-08-07T16:41:07Z)
• KAT-Coder-V2.5 Technical Report [61.907486544595336]
  KAT-Coder-V2.5 is a coding-focused agentic model trained to act autonomously inside real, executable repositories.<n>It reconstructs multilingual repositories into sandboxed environments with fail-to-pass and pass-to-pass verification at scale.<n>We further scale reinforcement learning with harness randomization, a reliability-hardened sandbox, an asymmetric actor--critic PPO with hindsight-augmented value estimation, and a harness-oriented reward framework.
  arXiv  Detail & Related papers  (2026-07-06T08:14:02Z)
• PairCoder++: Pair Programming as a Universal Paradigm for Verified Code-Driven Multimodal and Structured-Artifact Generation [51.92442051257354]
  PairCoder improves essentially every benchmark whose artifact is verifiable, on full official metric suites rather than execution alone.<n>TikZ compile rate up 10 to 30 points on every model, at 2.9 to 9.2 times single model cost.
  arXiv  Detail & Related papers  (2026-07-02T08:36:02Z)
• CIAware-Bench: Benchmarking Control Intervention Awareness Across Frontier LLMs [100.38986535324284]
  We introduce textbfCIAware-Bench, a benchmark for measuring textbfcontrol textbfintervention (CI) awareness across frontier models.<n>CIAware-Bench tests whether models can distinguish their own trajectories from those modified by a control intervention.
  arXiv  Detail & Related papers  (2026-06-09T16:24:16Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• WybeCoder: Verified Imperative Code Generation [22.401681809856896]
  WybeCoder is an agentic code verification framework.<n>It enables prove-as-you-generate development where code, invariants, and proofs co-evolve.
  arXiv  Detail & Related papers  (2026-03-31T00:06:44Z)
• An Agentic Evaluation Framework for AI-Generated Scientific Code in PETSc [7.236134946837382]
  petscagent-bench is an agentic framework built on an agents-evaluating-agents paradigm.<n>It orchestrates a 14-evaluator pipeline across five scoring categories: correctness, performance, code quality, algorithmic appropriateness, and library-specific conventions.<n>We demonstrate the framework on a benchmark suite of realistic problems using the PETSc library for HPC.
  arXiv  Detail & Related papers  (2026-03-16T22:46:10Z)
• ACE Runtime - A ZKP-Native Blockchain Runtime with Sub-Second Cryptographic Finality [1.7429038786735553]
  Existing high performance blockchains verify one signature per transaction on the critical path.<n>This paper presents ACE, a ZKP native execution layer built on identity authorization separation.
  arXiv  Detail & Related papers  (2026-03-10T21:39:36Z)
• Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
  silicon-grade correctness remains bottlenecked by: (i) limited test coverage and reliability of simulation-centric evaluation, (ii) regressions and repair hallucinations, and (iii) semantic drift as intent is reinterpreted across agent handoffs.<n>We propose Veri-Sure, a multi-agent framework that establishes a design contract to align agents' intent and uses a patching mechanism guided by static dependency slicing to perform precise, localized repairs.
  arXiv  Detail & Related papers  (2026-01-27T16:10:23Z)
• Every Step Counts: Decoding Trajectories as Authorship Fingerprints of dLLMs [63.82840470917859]
  We show that the decoding mechanism of dLLMs can be used as a powerful tool for model attribution.<n>We propose a novel information extraction scheme called the Directed Decoding Map (DDM), which captures structural relationships between decoding steps and better reveals model-specific behaviors.
  arXiv  Detail & Related papers  (2025-10-02T06:25:10Z)
• SVTRv2: CTC Beats Encoder-Decoder Models in Scene Text Recognition [77.28814034644287]
  We propose SVTRv2, a CTC model endowed with the ability to handle text irregularities and model linguistic context.<n>We extensively evaluate SVTRv2 in both standard and recent challenging benchmarks.<n> SVTRv2 surpasses most EDTRs across the scenarios in terms of accuracy and inference speed.
  arXiv  Detail & Related papers  (2024-11-24T14:21:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.