salle A. Turing CE4
5 mars 2012 - 14h00
Program Analysis and Machine Learning: A Win-Win Deal
par Sriram Rajamani de Microsoft Research
Abstract: We give an account of our experiences working at the intersection of two fields: program analysis and machine learning. In particular, we show that machine learning can be used to infer annotations for program analysis tools, and that program analysis techniques can be used to improve the efficiency of machine learning tools.
Every program analysis tool needs annotations. We show how such annotations can be derived from high level intuitions using Bayesian inference. In this approach, annotations are thought of as random variables, and intuitions of the programmer are stated as probabilistic constraints over these random variables. The Bayesian framework models and tolerates uncertainty in programmer intuitions, and Bayesian inference is used to infer most likely annotations, given the program structure and programmer intuitions. We give specific examples of such annotation inference for information and ownership types. We also describe a generic scheme to infer annotations for any safety property.
Machine learning algorithms perform statistical inference by analyzing voluminous data. Program analysis techniques can be used to greatly optimize these algorithms. In particular, statistical inference tools perform inference from data and first-order logic specifications. We show how Counterexample Guided Abstraction Refinement (CEGAR) techniques, commonly used in verification tools and theorem provers can be used to lazily instantiate axioms and improve the efficiency of inference.
In summary, we believe that these cross fertilization of ideas from program analysis and machine learning have the potential to improve both fields, resulting in a mutual win-win deal. We speculate on further opportunities for mutually beneficial exchange of ideas between the two fields.
joint work with Aditya Nori
