Circuit-Based Program Verification: Sequential Circuits as an Intermediate Representation for Verifying C Programs

• URL: http://arxiv.org/abs/2608.07397v1
• Date: Fri, 07 Aug 2026 16:41:07 GMT
• Title: Circuit-Based Program Verification: Sequential Circuits as an Intermediate Representation for Verifying C Programs
• Abstract summary: 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.
• Score: 5.82728420508304
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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.

Related papers

• Terminal Agents: A Survey of AI Agents in Command-Line Environments [102.48222742145474]
  Large language model agents increasingly act through terminals, yet existing surveys disperse terminal-mediated behavior across software engineering, tool use, and computer-use research.<n>We regard terminal agents as systems whose dominant progress-bearing action--observation loop is mediated by terminal command execution, textual feedback, and stateful environment interaction.<n>Our synthesis shows that realized behavior is jointly shaped by the model, interface, harness, runtime, and environment.
  arXiv  Detail & Related papers  (2026-08-20T18:16:44Z)
• Intent-Level Quantum Programming with Assertion-Guided Execution and Inspectable Intermediate Representation [0.22183164865527472]
  We present a quantum domain-specific language (Q) that addresses problems through three mechanisms.<n>First-class IR introspection, exposing circuit width, wire mapping, operation order, and measurement intent for developer inspection prior to execution.<n> assertion-guided modality inference, where the engine examines declared verification properties to automatically select sampling, statevector, or dual execution.
  arXiv  Detail & Related papers  (2026-07-31T18:21:32Z)
• BTOR2-Based C Program Verification via Hardware Model Checking [10.596871975682978]
  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.
  arXiv  Detail & Related papers  (2026-07-20T07:18:59Z)
• EquivFusion: Unifying Hardware Equivalence Checking from Algorithms to Netlists via MLIR [14.681439854488765]
  EquivFusion is an end-to-end equivalence checking tool tailored for multi-modal circuit designs.<n>It unifies diverse entry points, including PyTorch, C/C++, Chisel, Verilog, and gate-level netlists, into a common intermediate representation.
  arXiv  Detail & Related papers  (2026-04-17T12:09:54Z)
• UniDial-EvalKit: A Unified Toolkit for Evaluating Multi-Faceted Conversational Abilities [70.79422099851506]
  We present UniDial-EvalKit (UDE), a unified evaluation toolkit for assessing interactive AI systems.<n>UDE standardizes heterogeneous data formats into a universal schema, streamlines complex evaluation pipelines through a modular architecture, and aligns metric calculations under a consistent scoring interface.
  arXiv  Detail & Related papers  (2026-03-24T13:01:31Z)
• Scaling Agentic Verifier for Competitive Coding [66.11758166379092]
  Large language models (LLMs) have demonstrated strong coding capabilities but still struggle to solve competitive programming problems correctly in a single attempt.<n>Execution-based re-ranking offers a promising test-time scaling strategy, yet existing methods are constrained by either difficult test case generation or inefficient random input sampling.<n>We propose Agentic Verifier, an execution-based agent that actively reasons about program behaviors and searches for highly discriminative test inputs.
  arXiv  Detail & Related papers  (2026-02-04T06:30:40Z)
• 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)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  We provide a framework to encode system specifications and define corresponding certificates. We present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
  arXiv  Detail & Related papers  (2023-09-12T09:37:26Z)
• Adaptive Planning Search Algorithm for Analog Circuit Verification [53.97809573610992]
  We propose a machine learning (ML) approach, which uses less simulations. We show that the proposed approach is able to provide OCCs closer to the specifications for all circuits.
  arXiv  Detail & Related papers  (2023-06-23T12:57:46Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  We introduce the CoCoMoT (Computing Conformance Modulo Theories) framework. First, we show how SAT-based encodings studied in the pure control-flow setting can be lifted to our data-aware case. Second, we introduce a novel preprocessing technique based on a notion of property-preserving clustering.
  arXiv  Detail & Related papers  (2021-03-18T20:22:50Z)
• Controlled time series generation for automotive software-in-the-loop testing using GANs [0.5352699766206808]
  Testing automotive mechatronic systems partly uses the software-in-the-loop approach, where systematically covering inputs of the system-under-test remains a major challenge. One approach is to craft input sequences which eases control and feedback of the test process but falls short of exposing the system to realistic scenarios. The other is to replay sequences recorded from field operations which accounts for reality but requires collecting a well-labeled dataset of sufficient capacity for widespread use, which is expensive. This work applies the well-known unsupervised learning framework of Generative Adrial Networks (GAN) to learn an unlabeled dataset of recorded in-vehicle
  arXiv  Detail & Related papers  (2020-02-16T16:19:29Z)

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.