CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses

• URL: http://arxiv.org/abs/2510.26431v1
• Date: Thu, 30 Oct 2025 12:25:06 GMT
• Title: CHCVerif: A Portfolio-Based Solver for Constrained Horn Clauses
• Abstract summary: Constrained Horn Clauses (CHCs) are widely adopted as intermediate representations for verification tasks.<n>This paper introduces a portfolio-based CHC solver that adopts a software verification approach for solving CHCs.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Constrained Horn Clauses (CHCs) are widely adopted as intermediate representations for a variety of verification tasks, including safety checking, invariant synthesis, and interprocedural analysis. This paper introduces CHCVERIF, a portfolio-based CHC solver that adopts a software verification approach for solving CHCs. This approach enables us to reuse mature software verification tools to tackle CHC benchmarks, particularly those involving bitvectors and low-level semantics. Our evaluation shows that while the method enjoys only moderate success with linear integer arithmetic, it achieves modest success on bitvector benchmarks. Moreover, our results demonstrate the viability and potential of using software verification tools as backends for CHC solving, particularly when supported by a carefully constructed portfolio.

Related papers

• Foundational Constraint Solving for Expressive Refinement Typing [0.9624643581968987]
  We present FLEX, a Constrained Horn Clause (CHC) solver implemented in LEAN.<n>We show how FLEX reduces the trusted base to the kernel alone, and allows using LEAN's entire proof ecosystem to verify low-level systems code.
  arXiv  Detail & Related papers  (2026-07-14T00:15:23Z)
• ThinkBooster: A Unified Framework for Seamless Test-Time Scaling of LLM Reasoning [110.46431027868954]
  ThinkBooster is a framework for seamless test-time compute scaling of large language model (LLM) reasoning.<n>It consists of a modular Python library implementing state-of-the-art TTC scaling strategy and scorer families.<n>A deployable OpenAI-compatible proxy service enables drop-in integration of adaptive reasoning into real-world applications.
  arXiv  Detail & Related papers  (2026-06-05T05:28:46Z)
• Proof-of-Perception: Certified Tool-Using Multimodal Reasoning with Compositional Conformal Guarantees [2.8647133890966994]
  We present Proof-of-Perception (PoP), a tool-using framework that casts multimodal reasoning as an executable graph with explicit reliability guarantees.<n>PoP answers in verifiable evidence, reduces error compounding and hallucinations, and enables principled accuracy-compute trade-offs.
  arXiv  Detail & Related papers  (2026-02-27T21:35:12Z)
• Overcoming Joint Intractability with Lossless Hierarchical Speculative Decoding [58.92526489742584]
  We propose provably lossless.<n> verification method that significantly boosts the expected number of accepted tokens.<n>We show that HSD yields consistent improvements in acceptance rates across diverse model families and benchmarks.
  arXiv  Detail & Related papers  (2026-01-09T11:10:29Z)
• Theta as a Horn Solver [0.0]
  Theta is a verification framework that has participated in the CHC-COMP competition since 2023.<n>This paper provides a detailed description of the algorithms employed by Theta, highlighting the unique features that distinguish it from other CHC solvers.<n>We also analyze the strengths and weaknesses of the tool in the context of CHC-COMP benchmarks.
  arXiv  Detail & Related papers  (2025-10-30T12:24:52Z)
• On Continuous Optimization for Constraint Satisfaction Problems [33.35208489737497]
  Constraint satisfaction problems (CSPs) are fundamental in mathematics, physics, and theoretical computer science.<n>Recent advances show that modern continuous local search (CSP) solvers can achieve highly competitive results on certain classes of SAT problems.<n>We present a continuous optimization framework that generalizes the Walsh-Fourier transform to CSP, allowing for transforming versatile constraints to compact multi-intensives.
  arXiv  Detail & Related papers  (2025-10-06T04:30:07Z)
• Sample Efficient Certification of Discrete-Time Control Barrier Functions [2.4118840512344852]
  Control Invariant (CI) sets are instrumental in certifying the safety of dynamical systems.<n>Control Barrier Functions (CBFs) are effective tools to compute such sets, since the zero sublevel sets of CBFs are CI sets.<n>We present an approach to verify if the CBF actually satisfies the robust constraints.
  arXiv  Detail & Related papers  (2025-09-04T05:47:24Z)
• Semi-supervised Semantic Segmentation with Multi-Constraint Consistency Learning [81.02648336552421]
  We propose a Multi-Constraint Consistency Learning approach to facilitate the staged enhancement of the encoder and decoder.<n>Self-adaptive feature masking and noise injection are designed in an instance-specific manner to perturb the features for robust learning of the decoder.<n> Experimental results on Pascal VOC2012 and Cityscapes datasets demonstrate that our proposed MCCL achieves new state-of-the-art performance.
  arXiv  Detail & Related papers  (2025-03-23T03:21:33Z)
• Fast Context-Biasing for CTC and Transducer ASR models with CTC-based Word Spotter [57.64003871384959]
  This work presents a new approach to fast context-biasing with CTC-based Word Spotter. The proposed method matches CTC log-probabilities against a compact context graph to detect potential context-biasing candidates. The results demonstrate a significant acceleration of the context-biasing recognition with a simultaneous improvement in F-score and WER.
  arXiv  Detail & Related papers  (2024-06-11T09:37:52Z)
• LLMC: Benchmarking Large Language Model Quantization with a Versatile Compression Toolkit [55.73370804397226]
  Quantization, a key compression technique, can effectively mitigate these demands by compressing and accelerating large language models. We present LLMC, a plug-and-play compression toolkit, to fairly and systematically explore the impact of quantization. Powered by this versatile toolkit, our benchmark covers three key aspects: calibration data, algorithms (three strategies), and data formats.
  arXiv  Detail & Related papers  (2024-05-09T11:49:05Z)
• Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification [0.09786690381850355]
  Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA.
  arXiv  Detail & Related papers  (2024-04-23T16:46:27Z)
• Adaptive Hierarchical Certification for Segmentation using Randomized Smoothing [87.48628403354351]
  certification for machine learning is proving that no adversarial sample can evade a model within a range under certain conditions. Common certification methods for segmentation use a flat set of fine-grained classes, leading to high abstain rates due to model uncertainty. We propose a novel, more practical setting, which certifies pixels within a multi-level hierarchy, and adaptively relaxes the certification to a coarser level for unstable components.
  arXiv  Detail & Related papers  (2024-02-13T11:59:43Z)
• Multiple Query Satisfiability of Constrained Horn Clauses [0.0]
  We propose a technique that takes as input a set of CHCs, including a set of queries, and returns as output a new set of CHCs. The transformed CHCs incorporate in each new query suitable information coming from the other ones so that the CHC satisfiability algorithm is able to exploit the relationships among all queries.
  arXiv  Detail & Related papers  (2022-11-28T10:30:04Z)
• General Cutting Planes for Bound-Propagation-Based Neural Network Verification [144.7290035694459]
  We generalize the bound propagation procedure to allow the addition of arbitrary cutting plane constraints. We find that MIP solvers can generate high-quality cutting planes for strengthening bound-propagation-based verifiers. Our method is the first verifier that can completely solve the oval20 benchmark and verify twice as many instances on the oval21 benchmark.
  arXiv  Detail & Related papers  (2022-08-11T10:31:28Z)
• Using Representation Expressiveness and Learnability to Evaluate Self-Supervised Learning Methods [61.49061000562676]
  We introduce Cluster Learnability (CL) to assess learnability. CL is measured in terms of the performance of a KNN trained to predict labels obtained by clustering the representations with K-means. We find that CL better correlates with in-distribution model performance than other competing recent evaluation schemes.
  arXiv  Detail & Related papers  (2022-06-02T19:05:13Z)

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.