Invited speakers

Armin Biere

Institute for Formal Models and Verification, Johannes Kepler University

Bit-Blasting Considered Harmful

Bit-precise reasoning is essential for many automated reasoning tasks and
usually relies on SMT solvers for the theory of fixed-width bit-vectors.
After applying simplification through rewriting these solvers usually
rely on bit-blasting. The resulting propositional problem is then handed
to SAT solvers. On the theoretical side we discuss the complexity of
decision problems for bit-vectors. The main argument is that bit-blasting
is actually exponential. We discuss subclasses where the exponential
explosion is not immediate. On the practical side we show how to use
local search for bit-vectors, which avoids bit-blasting. This approach
is particularly effective on hard satisfiable bit-vector problems.

Roland Meyer

Department of Computer Science, TU Kaiserslautern

Summaries for Context-Free Games

(based on joint work with Lukas Holik and Sebastian Muskalla)

The motivation of our work is to generalize the language-theoretic approach from verification to
synthesis.
Central to language-theoretic verification are queries L(G) ⊆ L(A), where G is a context-free
grammar representing the flow of control in a recursive program and A is a finite automaton
representing (iterative refinements of) the specification.
When moving to synthesis, we replace the inclusion query by a strategy synthesis for an inclusion
game.
This means G comes with an ownership partitioning of the non-terminals.
It induces a game arena defined by the sentential forms and the left-derivation relation.
The winning condition is inclusion in the regular language given by A.

For the verification of recursive programs, the two major paradigms are summarization and saturation. Procedure summaries compute the effect of a procedure in the form of an input-output relation. Saturation techniques compute the pre*-image over the configurations of a pushdown system (including the stack). Both were extensively studied, optimized, and implemented. What speaks for summaries is that they seem to be used more often, as witnessed by the vast majority of verification tools participating in the software verification competition. The reason, besides simpler implementability, may be that the stack present in pre* increases the search space.

Saturation has been lifted to games and synthesis. We fill in the empty spot and propose the first summary-based solver and synthesis method for context-free inclusion games. Our algorithm is based on a novel representation of all plays starting in a non-terminal. The representation uses the domain of Boolean formulas over the transition monoid of the target automaton. The elements of the transition monoid are essentially procedure summaries. We show that our algorithm has optimal (doubly exponential) time complexity, that it is compatible with recent antichain optimizations, and that it admits a lazy evaluation strategy. Our preliminary experiments show encouraging results, indicating a speed up of three orders of magnitude over a competitor.

For the verification of recursive programs, the two major paradigms are summarization and saturation. Procedure summaries compute the effect of a procedure in the form of an input-output relation. Saturation techniques compute the pre*-image over the configurations of a pushdown system (including the stack). Both were extensively studied, optimized, and implemented. What speaks for summaries is that they seem to be used more often, as witnessed by the vast majority of verification tools participating in the software verification competition. The reason, besides simpler implementability, may be that the stack present in pre* increases the search space.

Saturation has been lifted to games and synthesis. We fill in the empty spot and propose the first summary-based solver and synthesis method for context-free inclusion games. Our algorithm is based on a novel representation of all plays starting in a non-terminal. The representation uses the domain of Boolean formulas over the transition monoid of the target automaton. The elements of the transition monoid are essentially procedure summaries. We show that our algorithm has optimal (doubly exponential) time complexity, that it is compatible with recent antichain optimizations, and that it admits a lazy evaluation strategy. Our preliminary experiments show encouraging results, indicating a speed up of three orders of magnitude over a competitor.

Luca Bortolussi

Department of Mathematics and Geosciences, University of Trieste

The machine learning way to formal verification

Many current scientific and technological challenges are related to understanding, design
and control of complex systems, from epidemic spreading to performance of computer systems, from
biological networks to bike and car sharing. Our interest is to study their emergent properties, starting
from a stochastic Markov model, with the machinery of formal verification. More precisely, the focus is
on the formalisation of such properties in a suitable logical language and on the automatic verification
of these properties in a given model (the so called model checking problem), which in a probabilistic
setting takes the form of computing the probability with which such properties are satisfied. However,
the models we can construct are always uncertain, in particular in the value of their parameters, due to
lack of information and their phenomenological nature. To deal consistently with such an uncertainty, we
have combined formal verification techniques with state-of-the-art Machine Learning statistical tools,
based on Gaussian Processes.

We will show how to efficiently compute the satisfaction probability of a behavioural property when model parameters are unknown, but assumed to lie in a bounded interval, a method we called Smoothed Model Checking. Combining these ideas with Bayesian Optimisation, we can then efficiently solve system design problems, i.e. fixing controllable model parameters so that the system robustly exhibits a desired behaviour. This talk will be a gentle introduction to these ideas.

We will show how to efficiently compute the satisfaction probability of a behavioural property when model parameters are unknown, but assumed to lie in a bounded interval, a method we called Smoothed Model Checking. Combining these ideas with Bayesian Optimisation, we can then efficiently solve system design problems, i.e. fixing controllable model parameters so that the system robustly exhibits a desired behaviour. This talk will be a gentle introduction to these ideas.