1,553 papers · page 21 of 78
Abstract We propose a spurious region guided refinement approach for robustness verification of deep neural networks. Our method starts with applying the DeepPoly abstract domain to analyze the network. If the robustness property cannot be verified, the result is inconclusive. Du…
Abstract We present an algorithm for extracting a subclass of the context free grammars (CFGs) from a trained recurrent neural network (RNN). We develop a new framework,pattern rule sets(PRSs), which describe sequences of deterministic finite automata (DFAs) that approximate a no…
Property-directed reachability (PDR) is a SAT/SMT-based reachability algorithm that incrementally constructs inductive invariants. After it was successfully applied to hardware model checking, several adaptations to software model checking have been proposed. We contribute a repl…
Abstract Verification algorithms are among the most resource-intensive computation tasks. Saving energy is important for our living environment and to save cost in data centers. Yet, researchers compare the efficiency of algorithms still in terms of consumption of CPU time (or ev…
Abstract VeriAbs is a strategy selection based reachability verifier for C code. It analyzes the structure of loops, and intervals of inputs to choose one of the four verification strategies implemented in VeriAbs. In this paper, we present VeriAbs version 1.4 with updates in thr…
In this paper we employ SMT solvers to soundly synthesise Lyapunov functions that assert the stability of a given dynamical model. The search for a Lyapunov function is framed as the satisfiability of a second-order logical formula, asking whether there exists a function satisfyi…
Boolean programs with multiple recursive threads can be captured as pushdown automata with multiple stacks. This model is Turing complete, and hence, one is often interested in analyzing a restricted class which still captures useful behaviors. In this paper, we propose a new cla…
Abstract We present the main concepts, components, and usage of G asol , a Gas AnalysiS and Optimization tooL for Ethereum smart contracts. G asol offers a wide variety of cost models that allow inferring the gas consumption associated to selected types of EVM instructions and/or…
Abstract We present an algorithm to decide the equivalence of context-free session types, practical to the point of being incorporated in a compiler. We prove its soundness and completeness. We further evaluate its behaviour in practice. In the process, we introduce an algorithm …
We present an algorithm for active learning of deterministic timed automata with a single clock. The algorithm is within the framework of Angluin’s $$L^*$$ algorithm and inspired by existing work on the active learning of symbolic automata. Due to the need of guessing for each tr…
Abstract We study identification in the limit using polynomial time and data for models of $$\omega $$ -automata. On the negative side we show that non-deterministic $$\omega $$ -automata (of types Büchi, coBüchi, Parity or Muller) can not be polynomially learned in the limit. On…
We introduce Mora , an automated tool for generating invariants of probabilistic programs. Inputs to Mora are so-called Prob-solvable loops, that is probabilistic programs with polynomial assignments over random variables and parametrized distributions. Combining methods from sym…
Abstract The Debian distribution includes more than 28 thousand maintainer scripts, almost all of them are written in Posix shell. These scripts are executed with root privileges at installation, update, and removal of a package, which make them critical for system maintenance. W…
In many areas of computer science, we are given an unsatisfiable set of constraints with the goal to provide an insight into the unsatisfiability. One of common approaches is to identify minimal unsatisfiable subsets (MUSes) of the constraint set. The more MUSes are identified, t…
Abstract We propose a novel algorithm for the solution of mean-payoff games that merges together two seemingly unrelated concepts introduced in the context of parity games, small progress measures and quasi dominions. We show that the integration of the two notions can be highly …
Abstract This report describes the 2020 Competition on Software Verification (SV-COMP), the 9 $$^{\text {th}}$$ edition of a series of comparative evaluations of fully automatic software verifiers for C and Java programs. The competition provides a snapshot of the current state o…
Abstract We present a programming language for describing and analysing concurrent quantum systems. We have an interpreter for programs in the language, using a symbolic rather than a numeric calculator, and we give its performance on examples from quantum communication and crypt…
We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata.
This paper introduces the statistical model checker FIGV, that estimates transient and steady-state reachability properties in stochastic automata. This software tool specialises in Rare Event Simulation via importance splitting, and implements the algorithms RESTART and Fixed Ef…
Dynamic fault trees (DFT) are widely adopted in industry to assess the dependability of safety-critical equipment. Since many systems are too large to be studied numerically, DFTs dependability is often analysed using Monte Carlo simulation. A bottleneck here is that many simulat…