26,098 papers · page 354 of 1,305
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…
Abstract Session types provide a principled programming discipline for structured interactions. They represent a wide spectrum of type-systems for concurrency. Their type safety is thus extremely important. EMTST is a tool to aid in representing and validating theorems about sess…
We present a full-program induction technique for proving (a sub-class of) quantified as well as quantifier-free properties of programs manipulating arrays of parametric size N . Instead of inducting over individual loops, our technique inducts over the entire program (possibly c…
Abstract Symbiotic 7 brings improvements in all parts of the tool. In particular, we integrated the advanced shape analysis implemented in Predator to our instrumentation process for memory safety checking. Further, we extended our slicer to correctly handle non-terminating progr…
The initialization of complex cyber-physical systems often requires the interaction of various components that must start up with strict timing requirements on the provision of signals (power, refrigeration, light, etc.). In order to safely allow an independent development of com…
We consider Markov decision processes (MDPs) in which the transition probabilities and rewards belong to an uncertainty set parametrized by a collection of random variables. The probability distributions for these random parameters are unknown. The problem is to compute the proba…
We consider the verification of multiple expected reward objectives at once on Markov decision processes (MDPs). This enables a trade-off analysis among multiple objectives by obtaining a Pareto front. We focus on strategies that are easy to employ and implement. That is, strateg…
Abstract Ultimate Taipan is a software model checker that combines trace abstraction with abstract interpretation on path programs. In this year’s version, we replaced our abstract interpretation engine and now use a combination of multiple abstraction functions, fixpoint computa…
We present KReach , a tool for deciding reachability in general Petri nets. The tool is a full implementation of Kosaraju’s original 1982 decision procedure for reachability in VASS. We believe this to be the first implementation of its kind. We include a comprehensive suite of l…