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.
Xinyu Zhang, Runxuan Fang, Ziqun Bao et al.· arXiv.org· 0 citations
The Maximum Satisfiability (MaxSAT) problem is a fundamental combinatorial optimization task, and state‐of‐the‐art solvers rely on decades of expert‐engineered heuristics and low‐level micro‐optimizations to achieve competitive performance. While recent Large Language Model (LLM)‐driven approaches (e.g., FunSearch, SATLUTION) have shown promise in algorithmic design and global solver evolution, they either focus on high‐level algorithmic sketches or large‐scale code restructuring, leaving the potential of purely local, correctness‐validated code optimization for industrial MaxSAT solvers largely underexplored in prior MaxSAT‐focused studies. This paper presents LoMax, a plug‐and‐play framework that leverages an LLM to perform local code optimization for MaxSAT solvers. Without any human‐written heuristics or instance‐specific domain‐specific templates (The prompts contain general MaxSAT domain knowledge but no instance‐specific or benchmark‐specific optimization templates), LoMax iteratively (i) ranks source files, (ii) scores individual functions, (iii) optimizes the highest‐scoring function body, (iv) performs a fast sanity evaluation on a small instance set, and (v) validates it on full exact‐unweighted and exact‐weighted benchmarks. Experiments on two state‐of‐the‐art solvers (UWrMaxSat‐SCIP‐MaxPre and OpenWBO) show consistent improvements: UWrMaxSat‐SCIP‐MaxPre solves +31$$ +31 $$ additional instances (average runtime 13.11 s →$$ \to $$ 14.27 s) on 553 unweighted instances and +23$$ +23 $$ additional solved instances (average runtime 11.67 s →$$ \to $$ 10.76 s) on 571 weighted instances, both under a uniform 100‐second timeout; OpenWBO solves +12$$ +12 $$ additional instances ( −8.9%$$ -8.9\% $$ average time) on 553 unweighted instances, providing empirical evidence that LLM‐driven local code rewriting can improve the performance of industrial MaxSAT solvers in the evaluated settings.
Fan Gao, Yanhong Huang, Jianwen Li et al.· Concurrency and Computation· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
