Microsoft Cibai is a generic static analyzer based on abstract interpretation for the modular analysis and verification of Java classes.
Many people are twittering and blogging about Microsoft’s Cibai. Being curious on what Microsoft have come up with, I read the Cibai paper.
In short, Cibai seeks to automatically verify object-oriented programs. This is in contrast to JUnit, where programmers have to manually write the test cases to test the programs.
Cibai first performs syntactic transformations of the code to an abstract syntax tree. Then Cibai analyzes the abstract syntax tree for dependencies across the classes and eventually infers class invariants, loops invariants and methods postconditions. Lastly, Cibai uses such information to prove the absence of certain runtime errors, such as divisions by zero, arrays out of bounds, null dereferences and simple user-provided assertions.
The next step in the development of Cibai is the generation of method summaries and applying Cibai on the Java API so to generate class/method stubs.
This is still a preliminary research paper. Given time, I am sure Microsoft would further develop Cibai. But think again, maybe not..