This article introduces a framework that is meant to assist in mitigating societal risks that software can pose. Concretely, this encompasses facets of software doping as well as unfairness and discrimination in high-risk decision-making systems.

We introduce the notion of porous invariants for multipath affine loops over the integers. These are invariants definable in (fragments of) Presburger arithmetic and, as such, lack certain tame geometrical properties, such a convexity and …

Markov chain analysis is a key technique in formal verification. A practical obstacle is that all probabilities in Markov models need to be known. However, system quantities such as failure rates or packet loss ratios, etc. are often not—or only …

Runtime Enforcement (RE) is a technique aimed at monitoring the executions of a system at runtime and ensure its compliance against a set of formal requirements (properties). RE employs an enforcer (a safety wrapper for the system) which modifies …

We consider the problem of proving termination for triangular weakly non-linear loops (twn-loops) over some ring $$\mathcal {S}$$ S like $$\mathbb {Z}$$ Z , $$\mathbb {Q}$$ Q , or $$\mathbb {R}$$ R . The guard of such a loop is an arbitrary …

The reference point for developing any artefact is its specification; to develop software formally, a formal specification is required. For sequential programs, pre and post conditions (together with abstract objects) suffice; rely and guarantee …

Parameterized programs are composed of an arbitrary number of concurrent, infinite-state threads. Automated safety and liveness proofs of such parameterized software are hard; state-of-the-art methods for their formal verification rely on …

Since 2013, the leading SAT solvers in SAT competitions all use inprocessing, which, unlike preprocessing, interleaves search with simplifications. However, inprocessing is typically a performance bottleneck, in particular for hard or large …

We consider systems with unboundedly many processes that communicate through shared memory. In that context, simple verification questions have a high complexity or, in the case of pushdown processes, are even undecidable. Good algorithmic …

GPUs offer parallelism as a commodity, but they are difficult to program correctly. Static analyzers that guarantee data-race freedom (DRF) are essential to help programmers establish the correctness of their programs (kernels). However, existing …

Sharp bisimulation is a refinement of branching bisimulation, parameterized by a subset of the system’s actions, called strong actions. This parameterization allows the sharp bisimulation to be tailored by the property under verification …

Quantifier bounding is a standard approach in inductive program synthesis to deal with unbounded domains. In this paper, we propose one such bounding method for the synthesis of recursive functions over recursive input data types. The synthesis …

Architecture specifications such as Armv8-A and RISC-V are the ultimate foundation for software verification and the correctness criteria for hardware verification. They should define the allowed sequential and relaxed-memory concurrency behaviour …

In many areas of computer science, we are given an unsatisfiable Boolean formula F in CNF, i.e. a set of clauses, with the goal to analyse the unsatisfiability. Examination of minimal unsatisfiable subsets (MUSes) of F is a kind of such analysis.

SMT-based model checkers, especially IC3-style ones, are currently the most effective techniques for verification of infinite state systems. They infer global inductive invariants via local reasoning about a single step of the transition relation …

Modern software development rarely takes place within a single programming language. Often, programmers appeal to cross-language interoperability. Examples are exploitation of novel features of one language within another, and cross-language code …

We study turn-based stochastic zero-sum games with lexicographic preferences over objectives. Stochastic games are standard models in control, verification, and synthesis of stochastic reactive systems that exhibit both randomness as well as …

First-order transition systems are a convenient formalism to specify parametric systems such as multi-agent workflows or distributed algorithms. In general, any nontrivial question about such systems is undecidable. Here, we present three …

We introduce a new property called robust reachability which refines the standard notion of reachability in order to take replicability into account. A bug is robustly reachable if a controlled input can make it so the bug is reached whatever the …