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.

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.