1,553 papers · page 11 of 78
Abstract Neural network verification mainly focuses on local robustness properties, which can be checked by bounding the image (set of outputs) of a given input set. However, often it is important to know whether a given property holds globally for the input domain, and if not th…
Abstract The L4 API (Application Programming Interface) is a core component of the operating system, which serves as the interface between user-level processes and the microkernel, facilitating communication and interaction. It is crucial to ensure the correctness and reliability…
Abstract We consider parameterized verification of systems executing according to the total store ordering (TSO) semantics. The processes manipulate abstract data types over potentially infinite domains. We present a framework that translates the reachability problem for such sys…
Abstract We present a framework for efficient stateless model checking (SMC) of concurrent programs under three prominent models of causal consistency, $${\texttt {CCv}}, {\texttt {CM}}, \texttt{CC}$$ CCv , CM , CC . Our approach is based on exploring traces under the program ord…
Abstract Parity games are two-player zero-sum games of infinite duration played on finite graphs for which no solution in polynomial time is still known. Solving a parity game is an $$\text{ NP }\cap \text{ co-NP }$$ NP ∩ co-NP problem, with the best worst-case complexity algorit…
Abstract Efficiency is a fundamental property of any type of program, but it is even more so in the context of the programs executing on the blockchain (known as smart contracts ). This is because optimizing smart contracts has direct consequences on reducing the costs of deployi…
Abstract Combining different verification and testing techniques together could, at least in theory, achieve better results than each individual one on its own. The challenge in doing so is how to take advantage of the strengths of each technique while compensating for their weak…
Abstract Deep reinforcement learning (DRL) has become a dominant deep-learning paradigm for tasks where complex policies are learned within reactive systems. Unfortunately, these policies are known to be susceptible to bugs. Despite significant progress in DNN verification, there…
Abstract We automatically compute a new class of environment assumptions in two-player turn-based finite graph games which characterize an “adequate cooperation” needed from the environment to allow the system player to win. Given an $$\omega $$ -regular winning condition $$\varP…
Abstract Proofs from SMT solvers ensure correctness independently from implementation, which is often a requirement when solvers are used in safety-critical applications or proof assistants. Alethe is an established SMT proof format generated by the solvers veriT and cvc5, with r…
Abstract We show how to generate a constraint system of symbolic expressions as part of an inter-procedural constraint-system–based program analysis such that any chosen slice of the intended analysis may be computed through the evaluation of the symbolic constraints. Thus, our m…
Abstract The new version of the witness validator Symbiotic-Witch follows more precisely the (fixed version of the) semantics of verification witnesses. This makes the tool more efficient as it can benefit from sink nodes. Further, the tool can now refute a witness. To sum up, Sy…
Abstract A hyperproperty relates executions of a program and is used to formalize security objectives such as confidentiality, non-interference, privacy, and anonymity. Formally, a hyperproperty is a collection of allowable sets of executions. A program violates a hyperproperty i…
Abstract We study a variant of the problem of synthesizing Mealy machines that enforce LTL specifications against all possible behaviours of the environment, including hostile ones. In the variant studied here, the user provides the high level LTL specification $$\varphi $$ of th…
Abstract With the rapid growth of machine learning, deep neural networks (DNNs) are now being used in numerous domains. Unfortunately, DNNs are “black-boxes”, and cannot be interpreted by humans, which is a substantial concern in safety-critical systems. To mitigate this issue, r…
Abstract Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite expected runtime. We contribute a simple yet effective inductive synthesis approach for proving such quantitative reachability properties b…
Abstract Numerical and symbolic methods for optimization are used extensively in engineering, industry, and finance. Various methods are used to reduce problems of interest to ones that are amenable to solution by these methods. We develop a framework for designing and applying s…
Abstract HyperLTL is a temporal logic that can express hyperproperties, i.e., properties that relate multiple execution traces of a system. Such properties are becoming increasingly important and naturally occur, e.g., in information-flow control, robustness, mutation testing, pa…
Abstract The 12th edition of the Competition on Software Verification (SV-COMP 2023) is again the largest overview of tools for software verification, evaluating 52 verification systems from 34 teams from 10 countries. Besides providing an overview of the state of the art in auto…
Abstract Across the broad research field concerned with the analysis of computational systems, research endeavors are often categorized by the respective models under investigation. Algorithms and tools are usually developed for a specific model, hindering their applications to s…