ABSTRACT. Neural network verification is active and rapidly maturing research area, with a growing ecosystem of solvers and tools. The VNN-LIB standard was introduced to support interoperability in this ecosystem, but Version 1.0 has several serious short-comings as a formal foundation: it lacks a precise syntax, semantics, and type system, offers limited expressivity, and relies on externally defined ONNX models whose semantics are informal and constantly evolving. The latter distinguishes VNN-LIB from established standards such as SMT-LIB, where queries are self-contained and have fixed semantics. In this paper we address these challenges by developing the theoretical foundations of VNN-LIB 2.0. Our key contribution is the introduction of the notion of a network theory, which abstractly characterises the minimal semantic interface required from a neural network model format. This abstraction enables VNN-LIB to be defined independently of any specific ONNX version while remaining compatible with evolving model representations. Building on this foundation, we present a formal syntax for a more expressive query language, a type system for it over the numeric domains provided by the network theory, and finally a formal semantics. To ensure internal consistency, the standard is mechanised in the Agda theorem prover. VNN-LIB 2.0 therefore provides robust and rigorous foundations for trustworthy neural network verification.

ABSTRACT. Formal verification is paramount for neural networks in safetycritical domains yet remains constrained by the trade-off between precision and scalability, especially with modern high frequency activation functions. However, the inherent NP-hardness of the problem forces a fundamental trade-off between scalability and precision in existing methods, which fail to adequately capture the high-frequency nonlinearities of modern activations. To address this, Quadratic Approximation based Verification via Fourier series and Taylor truncation (QAV-FT) is proposed as a framework unifying Fourier-enhanced quadratic approximation and Taylor remainder aware error control. Specifically: (i) A Fourierbased quadratic abstraction is formulated for arbitrary activations, with a rigorous error bound established via Jackson’s theorem and Lebesgue constant analysis; (ii) A second-order propagation scheme utilizing Lagrange remainder theory is devised to analytically derive sound, tight bounds with reduced symbolic complexity; and (iii) These mechanisms are integrated into a scalable full-network verification algorithm. Empirical results on MNIST-FC and other benchmarks demonstrate that QAV-FT achieves an average certification accuracy of 96.8% across complex activations like Swish, GELU, and Mish, with favorable accuracy and efficiency over comparable methods on partial models.

ABSTRACT. Research on neural network verification has traditionally emphasized scalability. However, recent invalidations of formally verified neural networks highlight soundness as an equally important goal. Pursuing inherent soundness, we present Rocq-NN-Roll, the first verified prover for real-valued piecewise-affine neural networks. Rocq-NN-Roll combines a network and its specification into a piecewise-affine function and reduces the verification task to solving linear inequalities over each polyhedral region. Verified in Rocq, it also provides the first automated proof support for neural networks in any interactive theorem prover, highlighting their still underexplored role in this field.

ABSTRACT. Formal verification of Semantic Segmentation Networks is challenging due to high-dimensional output spaces and cumulative over-approximation errors in deep architectures. Existing verification methods based on specific Star-set reachability suffer from either exponential state explosion (exact splitting) or excessive conservativeness (interval-based relaxation). In this work, we present ATKVerifier, a verification framework for SSNs operating on an abstract domain named constrained-star (C-star), which captures spatial dependencies within MaxPool receptive fields through explicit predicate constraints. Our framework features: (1) an adaptive top-K lower bound mechanism that dynamically encodes K potential maximizers based on layer depth and interval overlap, balancing precision and computational cost through parameter-free adaptation; (2) an adaptive affine upper bound exploiting linear relationships between top candidates to replace conservative constant bounds; (3) region-level completeness (RLC), a spatial robustness metric quantifying the integrity of verified contiguous object regions. Experiments on M2NIST with three SSN architectures (16~24 layers) demonstrate 8~25% improvement in robust IoU over the state-of-the-art tool NNV, with the improvement scaling with the network's depth. For the 24-layer architecture, ATKVerifier achieves 59.2% RLC versus 43.8% of NNV, certifying 35.2% more complete semantic objects.

ABSTRACT. Formal verification of transformers has become increasingly important due to their widespread deployment in safety-critical applications. Compared to classic neural networks, the inferences of transformers involve highly complex computations, such as dot products in self-attention layers, rendering their verification extremely difficult. Existing approaches explored over-approximation methods by constructing convex constraints to bound the output ranges of transformers, which can achieve high efficiency. However, they may sacrifice verification precision, and consequently introduce significant approximation error that leads to frequent occurrences of false alarms. In this paper, we propose a transformer verification approach that can achieve improved precision. At the core of our approach is a novel usage of ReLU, by which we represent a precise but non-linear bound for dot products such that we can further exploit the rich body of literature for convex relaxation of ReLU to derive precise bounds. We extend two classic approaches to the context of transformers, a rule-based one and an optimization-based one, resulting in two new frameworks for efficient and precise verification. We evaluate our approaches on different model architectures and robustness properties derived from two datasets about sentiment analysis, and compare with the state-of-the-art baseline approach. Compared to the baseline, our approach can achieve significant precision improvement for most of the verification tasks with acceptable compromise of efficiency, which demonstrates the effectiveness of our approach.

ABSTRACT. Decision tree ensembles (DTE) are a popular model for a wide range of AI classification tasks, used in multiple safety critical domains, and hence verifying properties on these models has been an active topic of study over the last decade. One such verification question is the problem of sensitivity, which asks, given a DTE, whether a small change in subset of features can lead to misclassification of the input. In this work, our focus is to build a quantitative notion of sensitivity, tailored to DTEs, by discretizing the input space of the model and enumerating the regions which are susceptible to sensitivity. We propose a novel algorithmic technique that can perform this computation efficiently, within a certified error and confidence bound. Our approach is based on encoding the problem as an algebraic decision diagram (ADD), and further splitting it into subproblems that can be solved efficiently and make the computation compositional and scalable. We evaluate the performance of our technique over benchmarks of varying size in terms of number of trees and depth, comparing it against the performance of model counters over the same problem encoding. Experimental results show that our tool XCount achieves significant speedup over other approaches and can scale well with the increasing sizes of the ensembles.

ABSTRACT. Shielding is a prominent model-based technique to ensure safety of autonomous agents. Classical shielding aims to ensure that some- thing bad never happens and comes with strong guarantees about safety and maximal permissiveness. However, shielding systems for probabilistic safety, where something bad can happen, but only with an acceptable probability, has proven more intricate. This paper presents a formal framework that conservatively extends classical shields to probabilistic safety. In this framework, we demonstrate the impossibility to preserve the strong guarantees, provide natural shields with weaker guarantees, and offline and online shield constructions that provide strong safety guarantees. The empirical evaluation highlights the practical advantage of the new shields as well as computational feasibility.

ABSTRACT. Large Language Models perform well at natural language interpretation and reasoning, but their inherent stochasticity limits their adoption in regulated industries like finance and healthcare that operate under strict policies. To address this limitation, we launched Automated Reasoning checks (ARc): a public service that (1) uses LLMs with optional human guidance to formalize natural language policies, allowing fine-grained control of the formalization process, and (2) uses inference-time autoformalization to validate logical correctness of natural language statements against those policies. When correctness is paramount, we perform multiple redundant formalization steps at inference time, checking the formalizations for semantic equivalence. Our benchmarks show that ARc exceeds 99% soundness and achieves a near-zero false positive rate in identifying logical validity. Our approach produces auditable artifacts that substantiate the verification outcomes and can be used to improve the original text. ARc is the first commercial offering from a major cloud provider to integrate automated reasoning into a generative AI guardrail.

ABSTRACT. We introduce a generic certificate format for verifying liveness properties in hardware model checking, relying purely on propositional predicates and not involving explicit counters. Our certificates can be efficiently validated via a fixed number of SAT checks. The proposed format is compatible with state-of-the-art liveness checking algorithms. We present certificate generation for several representative techniques, including rLive, liveness-to-safety reduction, and k-liveness, as well as for a preprocessing method based on stabilizing constraint extraction. Experimental results on benchmarks from the Hardware Model Checking Competition demonstrate that our approach is practically effective with very low certification overhead, and our certificate checker was able to successfully validate all certificates that were generated.

ABSTRACT. Whenever automated provers such as automatic software verifiers deliver a verdict (true or false), they are expected to produce also a witness that justifies the verdict. This allows independent validation of the verdict using the witness by a third party, increasing trust in the results. The current standard exchange formats for witnesses in software verification do not support program termination. To fill this gap, we propose an extension of the witness format that is based on transition invariants as a general and effective formalism. We justify this by (a) proving that transition invariants can encode other popular termination arguments like ranking functions and (b) providing three different validation approaches for transition invariants, which together can validate most of the exported witnesses. Our approach based on transition invariants was integrated into version 2.1 of the recently released witness format, and the software-verification community has adopted the format for SV-COMP.

ABSTRACT. KoAT is a tool to automatically infer complexity bounds and prove termination of (possibly recursive) integer programs. To this end, KoAT implements an alternating modular inference of upper runtime and size bounds for program parts. In particular, KoAT uses a portfolio of different techniques to analyze subprograms. The power of our approach is demonstrated by an extensive experimental evaluation.

ABSTRACT. Verifying stateful software systems remains challenging due to complex control structures and intricate state interactions, often necessitating pre-existing behavioral models. We introduce Seal, an abstract interpreter that automatically derives sound and precise symbolic finite automata models. In tests on real-world applications, Seal generates sound and precise automata within minutes and, when employed in dynamic model checking, uncovers fifteen previously unknown bugs. These findings demonstrate that our approach can effectively connect code to model-based verification for stateful software systems.

ABSTRACT. We study the fully automated amortised cost analysis of purely functional data structures like skew heaps, as well as weight- and rank-biased leftist heaps. For that we generalise earlier works on automated amortised resource analysis by developing a type inference based approach based on a generic type system. This allows for modular reasoning and the inference of precise and optimal cost bounds. More specifically, we extend the work on the ATLAS system by Leutgeb et al., which was developed to cover the analysis of splay trees and some closely related data structures. To enable the analysis of skew heaps, however, and the even more challenging (amortized) analysis of leftist heaps, we have developed a range of new techniques for type-based automated analysis. By introducing a generic type system we allow for arbitrary (classes of) potential functions, compared to the use of hard-coded potential functions in ATLAS, which we have implemented in Haskell in an entirely modular way. We have also greatly enhanced the existing type inference algorithm by extensions in multiple directions, including path-sensitive reasoning, data structure invariants, and template parameters for piecewise defined potential functions. We show how our newly developed system supports the use of all known potential functions for analyzing skew heaps and leftists heaps, confirming the known bounds.

ABSTRACT. In numeric-intensive computations, it is well known that the execution of floating point programs is imprecise as floating point arithmetic incurs round-off errors. Although round-off errors are small for a single floating point operation, the aggregation of such errors may be dramatic and cause catastrophic program failures. Therefore, to ensure the correctness of floating point programs, round-off error needs to be carefully taken into account. In this work, we consider polynomial invariant generation for floating point programs, aiming at generating tight invariants under the perturbation of round-off errors. Our contribution is a novel framework for applying polynomial constraint solving to address the invariant generation problem, which is also the first polynomial constraint solving based approach that handles floating point errors to our best knowledge. In our framework, we propose a novel combination of round-off error analysis and polynomial constraint solving, aiming to circumvent the cost of handling a large number of error variables in the floating point model. Experimental results over a variety of challenging benchmarks show that our framework outperforms SOTA approaches in both time efficiency and the precision of generated invariants.

ABSTRACT. We present a parallel abstract interpretation technique for polynomial programs with assertions presented as unions of range bound constraints. We use the powerset domain of hyper-rectangles to over-approximate sets of reachable states. Our key technical contributions include novel abstract transformers and refinement operators that account for the semantics of polynomial assignments and guards more precisely than earlier work, while remaining amenable to parallelization and efficient implementation. This is achieved by appealing to Farkas' Lemma and Handelman's Theorem, and by exploiting geometric properties of unions of hyper-rectangles. Our abstract interpretation technique proves safety properties of many polynomial programs that state-of-the-art abstract interpretation tools fail to prove. We have implemented our approach in a tool called PolyAbs, and experimentally evaluated it on a suite of benchmarks. Our experiments demonstrate the improved precision and broader coverage of PolyAbs vis-a-vis state-of-the-art abstract interpretation tools, including a commercial-grade tool.

ABSTRACT. Several extensions of Datalog perform probabilistic inference by allowing users to annotate input facts and rules with probabilities. While extremely useful in many domains (e.g., quantitative program analysis), existing systems typically do not support incremental inference, meaning that even small changes trigger costly recomputation from scratch. This paper presents PINQ, the first incremental solving framework for probabilistic Datalog. Given a previously solved program and a set of changes, PINQ updates query probabilities by reusing the old derivation graphs and compiled decision diagrams. The key idea is to translate structural changes into parametric updates whenever sound to avoid redundant recomputation. Our framework combines an incremental derivation graph construction algorithm with an adaptive BDD construction technique that safely reuses existing BDDs via weight calibration whenever possible. Experimentally, PINQ achieves an average speedup of 17X over recomputation from scratch on a representative set of program analysis benchmarks.

ABSTRACT. Reference counting bugs in Linux kernel drivers can lead to severe resource mismanagement and security vulnerabilities. We intro- duce DrvHorn, a novel automated tool to detect these bugs by reducing reference counting verification to an assertion checking problem leverag- ing the Linux driver interface. Through efficient modeling of the Linux kernel and aggressive program slicing, DrvHorn discovered 545 bugs, of which 424 were previously unknown, across all platform drivers in v6.6 Linux kernel, with a lower false positive rate of 29.9% compared to prior studies. To address the root causes of these newly discovered bugs, we submitted patches to the Linux kernel, and 45 of them were merged.