Learning algorithms and formal verification

This tutorial is on applications of computational learning theory to verification of systems. Computational learning theory deals with algorithmic models for learning formally representable concepts using either positive and negative samples or by access to an oracle that can answer certain queries about the concept. The problem of learning formal languages has been particularly useful in verification applications. We will introduce Angluin's algorithm, a learning algorithm that learns regular languages efficiently using an oracle that can answer membership and equivalence queries. We will also survey results on learning regular languages in other learning models. We will give an account of how learning has been used to solve a variety of problems in verification, spanning compositional verification, parameterized model-checking, synthesis of interfaces, machines with unbounded queues, and program testing. In all these examples, a crucial property that is exploited is the simplicity of certain concepts that underlie real-world systems, the learning of which yields a a simple mechanism to prove the correctness of the system. We will also lay out general arguments on why learning algorithms can play a crucial role in the design of verification algorithms, and list some open research directions that work towards this goal.