Seminar by Aditya Nori
Program Verification via Machine Learning
Aditya Nori
Microsoft Research, Bangalore
Date: Monday, September 2nd, 2013
Time: 5 PM
Venue: CS101.
Abstract:
In this talk, I will describe our experiences using machine learning techniques for computing proofs for assertion validation as well as program termination. Our main technical insights are: a) that interpolants in program verification can be viewed as classifiers in supervised machine learning, and b) loop bounds can be computed using linear regression. This view has the advantage that we are able to use off-the-shelf classification as well as regression techniques for proving safety as well as termination. Furthermore, we can also use data generated from existing test suites for programs in order to compute both safety and termination proofs. We demonstrate the feasibility of our techniques via experiments over several benchmarks from various papers on program verification.
About the speaker:
Aditya Nori is a member of the programming languages and machine learning groups at Microsoft Research India. He is also an adjunct professor at IIT Hyderabad. His research interests include algorithms for the analysis of programs and machine learning with special focus on tools for improving software reliability and programmer productivity. He received his PhD in Computer Science from the Indian Institute of Science, Bangalore.