Machine Learning Meets Formal Methods

In this talk, I will make the case that formal methods and machine learning indeed complement each other extremely well. As a gentle introduction to this area of research, I will present two of my current student projects. The first project uses formal methods to prove properties of an artificial neural network obtained from
Caenorhabditis Elegans, a nematode (worm) whose brain and nervous system have been completely mapped. The second project applies machine learning techniques to formal methods with the goal of identifying algorithms based on how they modify the memory.

In the second part of this talk, I will present a novel machine learning setting, called ICE learning, which we have developed for learning correctness proofs of software. Moreover, I will illustrate how ICE learning can be used to automatically verify various types of programs and discuss its application to other infinite-state systems.

I will conclude my talk with an outline of future research directions.