Probabilistic, Modular and Scalable Inference of Typestate Specifications

Today I presented my paper, Probabilistic, Modular and Scalable Inference of Typestate Specifications at PLDI 2011. This paper was joint work with Aditya Nori from Microsoft Research India. This was the second time I worked on a research project with Aditya, and as before our collaboration was extremely fruitful.

This paper is all about specification inference. The tool that I worked on for my thesis, Plural, checks that objects in a program are used according to their protocols. While the tool was quite powerful, it required a number of pre and post-conditions to verify that the protocol was being used correctly.

Our tool, Anek, infers them automatically, and does so using probabilistic constraints. This allows us to use various forms of evidence, some of which may conflict, in determining a final specification.

Anywho, the paper and presentation are now available online. Enjoy!