Tutorials

We will have two half-day tutorials:

Joost-Pieter Katoen (RWTH Aachen University and University of Twente)

Joost-Pieter Katoen

The What, Why, and How of Probabilistic Verification.

Abstract:
Probabilities are ubiquitous.  They are used in autonomous computing, systems biology, security, machine learning, to mention a few.  This tutorial addresses how verification techniques can be used to jointly address correctness and probabilities.  I’ll give a gentle introduction to what probabilistic verification is, why it is practically relevant and how it can be employed in practice.  I’ll conclude by addressing the main trends and challenges such as parametric verification, model repair, probabilistic programming etc. Tutorial material.
Slides: Part 1, Part 2, Part 3, Part 4.

Madhusudan Parthasarathy and Pranav Garg (University of Illinois at Urbana-Champaign)

Madhu Parthasarathy        Pranav Garg

Machine-learning based methods for synthesizing invariants.

Abstract:
Machine learning [1] has been recently applied to build effective algorithms for problems in verification and synthesis of systems. The first part of the tutorial covers basic machine learning concepts including the different learning problems (in particular, classifiers), various learning models, and known efficient learning algorithms. The second part of the tutorial will focus on how these learning algorithms have been recently adapted [2,3] to solve problems in program verification, with a focus on invariant synthesis. In particular, we will explore new learning models required for invariant generation and synthesis of program expressions, and how traditional machine-learning algorithms can be modified to these new learning models. We will also present a concrete learning algorithm that learns Boolean combinations of predicates that researchers can use to build their own invariant-synthesis engines. Tutorial material.

[1] T. M. Mitchell. Machine learning. McGraw Hill series in Computer Science. McGraw-Hill, 1997.
[2] R. Sharma, A. V. Nori, and A. Aiken. Interpolants as classifiers. In CAV 2012, LNCS, vol. 7358, Springer, 2012, pp. 71–87.
[3] P. Garg, D. Neider, P. Madhusudan, C. Loding. Learning Invariants using Decision Trees and Implication Counterexamples. UIUC Technical Report, May 2015.