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.