Specification Inference and Invariant Generation: A Machine Learning Perspective
Computing good specification and invariants is key to effectiveand efficient program verification. In this talk, I will describeour experiences in using machine learning techniques (Bayesianinference, SVMs) for computing specifications and invariantsuseful for program verification. The first project Merlin usesBayesian inference in order to automatically infer securityspecifications of programs. A novel feature of Merlin is that itcan infer specifications even when the code under analysis givesrise to conflicting constraints, a situation that typicallyoccurs when there are bugs. We have used Merlin to infer securityspecifications of 10 large business critical webapplications. Furthermore, we show that these specifications canbe used to detect new information flow security vulnerabilitiesin these applications.In the second project Interpol, we show how interpolants can beviewed as classifiers in supervised machine learning. This viewhas several advantages: First, we are able to use off-the-shelfclassification techniques, in particular support vectormachines (SVMs), for interpolation. Second, we show that SVMs canfind relevant predicates for a number of benchmarks. Sinceclassification algorithms are predictive, the interpolantscomputed via classification are likely to be relevant predicatesor invariants. Finally, the machine learning view also enables usto handle superficial non-linearities. Even if the underlyingproblem structure is linear, the symbolic constraints can give animpression that we are solving a non-linear problem. Sincelearning algorithms try to mine the underlying structuredirectly, we can discover the linear structure for suchproblems. We demonstrate the feasibility of Interpol viaexperiments over benchmarks from various papers on programverification.