| Abstract |
In this talk, I will present a static analysis, based on abstract interpretation, for automatic inference of class invariants in Object-Oriented languages. Class invariants are properties of classes valid before and after the execution of any public method of the class. I use this invariants for verifying the absence of runtime errors in Java programs.
I will present the underlying theory, the abstract domain, and a demo of Cibai, the tool I have designed and implemented. I will discuss the benefits of my approach which, unlike analogous tools is (1) sound (unlike ESC/Java 2 or Daikon), (2) Does not require interaction with a theorem prover (unlike Jive or Loop), and (3) Does not require user annotations (unlike Jack, Jakarta or Spec# in the C# world). |
