26,098 papers · page 307 of 1,305
This paper proposes a concurrency model for JavaScript with thread-like abstractions and cooperative cancellation. JavaScript uses an event-driven model, where an active computation runs until it completes or blocks for an event while concurrent computations wait for other events…
Abstract SV-COMP 2021 is the 10th edition of the Competition on Software Verification (SV-COMP), which is an annual comparative evaluation of fully automatic software verifiers for C and Java programs. The competition provides a snapshot of the current state of the art in the are…
Abstract It is well-known that the winning region of a parity game with n nodes and k priorities can be computed as a k-nested fixpoint of a suitable function; straightforward computation of this nested fixpoint requires $$\mathcal {O}(n^{\frac{k}{2}})$$ O ( n k 2 ) iterations of…
Abstract A smart contract is a program executed on a blockchain, based on which many cryptocurrencies are implemented, and is being used for automating transactions. Due to the large amount of money that smart contracts deal with, there is a surging demand for a method that can s…
Abstract To ensure a high availability, communication networks provide resilient routing mechanisms that quickly change routes upon failures. However, a fundamental algorithmic question underlying such mechanisms is hardly understood: how to verify whether a given network reroute…
Abstract Deductive verification has been successful in verifying interesting properties of real-world programs. One notable gap is the limited support for floating-point reasoning. This is unfortunate, as floating-point arithmetic is particularly unintuitive to reason about due t…
Abstract Gazer-Theta is a software model checking toolchain including various analyses for state reachability. The frontend, namely Gazer, supports C programs through an LLVM-based transformation and optimization pipeline. Gazer includes an integrated bounded model checker (BMC) …
Abstract Deep learning has emerged as an effective approach for creating modern software systems, with neural networks often surpassing hand-crafted systems. Unfortunately, neural networks are known to suffer from various safety and security issues. Formal verification is a promi…
Abstract We study semi-algorithms to synthesise the constraints under which a Parametric Timed Automaton satisfies some liveness requirement. The algorithms traverse a possibly infinite parametric zone graph, searching for accepting cycles. We provide new search and pruning algor…
Abstract Our submission to SV-COMP’21 is based on the software verification framework "Image missing" and implements the extension to the thread-modular approach. It considers every thread separately, but in a special environment which models thread interactions. The environment …
Abstract This paper presents a novel method for the automated synthesis of probabilistic programs. The starting point is a program sketch representing a finite family of finite-state Markov chains with related but distinct topologies, and a reachability specification. The method …
Abstract Recent advances have shown how decision trees are apt data structures for concisely representing strategies (or controllers) satisfying various objectives. Moreover, they also make the strategy more explainable. The recent tool had provided pipelines with tools supportin…
Abstract Many probabilistic inference problems such as stochastic filtering or the computation of rare event probabilities require model analysis under initial and terminal constraints. We propose a solution to thisbridging problemfor the widely used class of population-structure…
Abstract We introduce , a new proof format for unsatisfiable SAT problems, and its associated toolchain. Compared to , the format allows solvers to include more information in proofs to reduce the computational cost of subsequent elaboration to . The format is easy to parse forwa…
Abstract Several problems in planning and reactive synthesis can be reduced to the analysis of two-player quantitative graph games.Optimizationis one form of analysis. We argue that in many cases it may be better to replace the optimization problem with thesatisficing problem, wh…
Abstract Timed automata (TA) have shown to be a suitable formalism for modeling real-time systems. Moreover, modern model-checking tools allow a designer to check whether a TA complies with the system specification. However, the exact timing constraints of the system are often un…
Abstract Problems arising in many scientific disciplines are often modelled using edge-coloured directed graphs. These can be enormous in the number of both vertices and colours. Given such a graph, the original problem frequently translates to the detection of the graph’s strong…
Abstract This paper is about shipping runtime verification to the masses. It presents the crucial technology enabling everyday car owners to monitor the behaviour of their cars in-the-wild. Concretely, we present an Android app that deploys rtlola runtime monitors for the purpose…
Abstract We introduce a generalization of the bisimulation game that can be employed to find all relevant distinguishing Hennessy–Milner logic formulas for two compared finite-state processes. By measuring the use of expressive powers, we adapt the formula generation to just yiel…
Abstract Numerous tasks in program analysis and synthesis reduce to deciding reachability in possibly infinite graphs such as those induced by Petri nets. However, the Petri net reachability problem has recently been shown to require non-elementary time, which raises questions ab…