ABSTRACT. In the past two decades, significant research and development effort went into the development of verification tools for individual languages, such as C, C++, and Java. Many of the used verification approaches are in fact language-agnostic and it would be beneficial for the technology transfer to allow for using the implementations also for other programming and modeling languages. To address the problem, we propose SV-LIB, an exchange format and intermediate language for software-verification tasks, including programs, specifications, and verification witnesses. SV-LIB is based on well-known concepts from imperative programming languages and uses SMT-LIB to represent expressions and sorts used in the program. This makes it easy to parse and to build into existing infrastructure, since many verification tools are based on SMT solvers already. Furthermore, SV-LIB defines a witness format for both correct and incorrect SV-LIB programs, together with means for specifying witness-validation tasks. This makes it possible both to implement independent witness validators and to reuse some verifiers also as validators for witnesses. This paper presents version 1.0 of the SV-LIB format, including its design goals, the syntax, and informal semantics. Formal semantics and further extensions to concurrency are planned for future versions. This paper has already been published as a technical report on arXiv (https://arxiv.org/pdf/2511.21509) so we aim for a presentation-only paper.

ABSTRACT. Why3 relies on logical task transformations both for the translation of verification conditions to- wards external provers and for interactive proof. The kind of metalogical programming involved in these transformations is naturally expressed in higher-order logic programming languages such as λProlog. This paper presents Why3-Elpi, a tool that exposes a typed fragment of the Why3 API to λProlog using Elpi and lets users implement Why3 transformations in λProlog. This provides an environment where non-trivial transformations can be easily prototyped and experimented with, using a declarative and concise style.

ABSTRACT. WebAssembly is a stack-based imperative language widely used to develop safe and efficient Web applications. In this paper, we propose an automated static verification method for a subset of WebAssembly using a constrained Horn clauses (CHCs) satisfiability solver. Our main challenges are how to handle indirect function calls effectively and how to analyze huge panic handlers. A naïve approach to the former problem would be to model a function reference table as an array of functions' entry points, but it would suffer from having too many candidates for indirect calls, resulting in a large case analysis. We address the problem by utilizing type information and filtering candidates for each indirect function call. For the latter problem, a panic handler, which is a function that is called when an error occurs, can be very large and complex. We mitigate this problem by summarizing the panic handler using control-flow analysis. We confirmed the effectiveness of our approach through preliminary experiments.

ABSTRACT. Program safety verification with bit-precise semantics can naturally be encoded as Constrained Horn Clauses (CHCs) modulo the theory of fixed-size bit-vectors (T_B). Alternatively, bit-precise semantics can be encoded as CHCs modulo the theory of Integer Arithmetic (T_I) by modeling modular and bit-wise behavior using arithmetic constraints. However, neither approach consistently yields an efficient verification procedure: reasoning directly in T_B often limits the generalization capabilities of CHC solvers, whereas bit-precise T_I encodings produce complex arithmetic constraints that are expensive to process, especially in the presence of bit-wise operations. We present Mosaic, a theory-modular framework for deciding satisfiability of CHCs modulo T_B through modular reasoning in T_B and T_I. Given a CHC set modulo T_B, Mosaic partitions the input into a bit-vector fragment and an integer fragment, and exchanges information between them through sound theory transformations. This avoids committing the entire CHC set to a single theory, allowing different CHCs to be handled in different background theories. We implemented a prototype of Mosaic using Z3 and Spacer and evaluated it on bit-manipulating benchmarks. Our evaluation shows that Mosaic significantly outperforms both pure bit-vector and fully arithmetic CHC-solving approaches, often scaling to substantially larger bit-widths.

ABSTRACT. For high-assurance software, source-level reasoning is insufficient: we need binary-level guarantees. Despite constrained Horn clause (CHC) solving being one of the most popular forms of automated verification, prior work has not evaluated the viability of CHC solving for binary analysis. To fill this gap, we assemble a pipeline that encodes binary analysis problems as CHCs in the SMT logic of quantifier-free bit vectors, and show that off-the-shelf CHC solvers achieve reasonable success on binaries compiled from 983 C invariant inference benchmarks: a portfolio solves 59.5% and 66.0% of the problems derived from the unoptimized and optimized binaries, respectively—roughly equal to the success rate of a leading C verifier on the source code (60.1%). Moreover, we show that binary analysis provides a valuable source of bit-vector CHC benchmarks (which are in short supply): binary-derived problems differ from existing benchmarks both structurally and in solver success rates and rankings. Augmenting CHC solving competitions with binary-derived benchmarks will encourage solver developers to improve bit-vector reasoning, in turn making CHC solving a more effective tool for binary analysis.