2,069 papers · page 1 of 104
Abstract Remote Direct Memory Access (RDMA) is a technology that allows direct memory access from the memory of one computer into that of another without involving either one’s operating system. This enables high-throughput, low-latency networking, which is especially useful in m…
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 in…
Abstract Research on neural network verification has traditionally emphasized scalability. However, recent invalidations of formally verified results of neural networks highlight soundness as an equally important goal. Pursuing inherent soundness, we present Rocq-NN-Roll , the fi…
Abstract We present Kofola , an efficient tool for complementation and inclusion checking of Büchi automata, two central tasks in automata-theoretic verification with applications in model checking, monitoring, and theorem proving. Kofola implements a state-of-the-art modular com…
Abstract Large Language Models perform well at natural language interpretation and reasoning, but their lack of formal correctness guarantees limits their adoption in regulated industries like finance and healthcare that operate under strict policies. To address this limitation, …
Abstract We study the problem of generating paths on a graph that satisfy a collection of $$\omega $$ ω -regular objectives. We propose a decoupled framework in which each objective is assigned to an independent agent that selects a local policy, while a scheduler—oblivious to th…
Abstract Recent years have seen a significant increase in the interest in reactive synthesis from specifications that relate to infinite state spaces. We present , a tool for synthesis of infinite-state Linear Integer Arithmetic reactive systems. implements a CEGAR approach, rely…
Abstract We present PyCHC , a solver-agnostic framework aimed at systems of constrained Horn clauses (CHC). PyCHC provides intuitive Python APIs to create and manipulate CHC systems programmatically, and solve them using different backend solvers. Furthermore, PyCHC offers a cert…
Abstract We consider the problem of controlling a multi-mode system with respect to a safety goal in the Filippov sliding-mode semantics. When the goal can be enforced, we present a symbolic algorithm that enhances the previously known solution. When the goal cannot be enforced, …
Abstract Whenever automatic software verifiers determine that a program fulfills or violates its specification, they are expected to produce also a witness that justifies the verdict. This allows a third party to independently validate the verdict and the arguments from which it …
Abstract SvLibChecker is a small tool for software model checking. Its goal is to provide a light-weight framework that makes it easy to implement and explore algorithms for software verification. The input to SvLibChecker is an SV-LIB program. SV-LIB is an intermediate language …
Abstract Lagrangian-based duality, traditionally applied in optimization, has recently been generalized to serve as the basis for a unifying framework for primal-dual search algorithms in the context of program verification and automated reasoning. In this paper, we analyze Quant…
Abstract We show how to use passive automata learning to infer models of attacker-defender interactions in cybersecurity. By treating system event logs as words in a formal language, we can apply algorithms such as RPNI to infer compact deterministic finite automata from observed…
Abstract We study concurrent graph games where n players cooperate against an opponent to reach a set of target states. Unlike traditional settings, we study distributed randomisation: team players do not share a source of randomness, and their private random sources are hidden f…
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 …
Abstract We present a tool for the compositional verification and correct-by-construction synthesis of stochastic world models —heterogeneous networks of interdependent stochastic models including discrete and continuous-time Markov chains, Markov decision processes (MDPs), parti…
Abstract Computing optimal conditional reachability probabilities in Markov decision processes (MDPs) is tractable by a reduction to reachability probabilities. Yet, this reduction yields cyclic, challenging MDPs that are often notoriously hard to solve. We present an alternative…
Abstract Partially Observable Markov Decision Processes (POMDPs) are the standard framework for decision-making under uncertainty. While sampling-based methods scale well, they lack formal correctness guarantees, making them unsuitable for safety-critical applications. Conversely…
Abstract We present ZipLex , a verified framework for invertible linear-time lexical analysis following the longest match (maximal munch) semantics. Unlike past verified lexers that focus only on satisfying the semantics of regular expressions and the longest match property, ZipL…
Abstract This paper investigates the algorithmic safety verification problem of infinite-state parameterized concurrent programs over a rich set of communication topologies. The goal is to automatically produce a proof of correctness in the form of a universally quantified induct…