Abstract:

The talk will outline applications of machine learning in formal verification. In the Learning to Verify project, we have been exploring an approach to model checking wherein the model-checking problem is viewed as a learning problem. For example, the problem of verifying invariants is viewed as a problem of learning the set of reachable states. The talk will outline how this approach can be used to verify properties with respect to expressive specification logics like LTL and CTL. The ideas have been implemented using Angluin's L* algorithm for learning regular languages in a tool called Lever. The last part of the talk will address the problem of learning pushdown models, and present recent results in this context. We will conclude with applications of this learning algorithm to perform black-box checking, compositional verification, and learning to verify.

Mahesh Viswanathan obtained his bachelor's degree in computer science from the Indian Institute of Technology at Kanpur in 1995, and his doctorate from the University of Pennsylvania in 2000. He was a post-doctoral fellow at DIMACS with a joint appointment at Telcordia Technologies in 2000-01. Since 2001, he has been an Assistant professor at the University of Illinois at Urbana-Champaign. His research interests are in the core areas of logic, automata theory, and algorithm design, with applications to the algorithmic verification of systems.