We introduce a generic static analyzer based on abstract interpretation for the modular analysis and verification of Java classes. We present the abstract semantics and the underlying abstract domain, a combination of an aliasing analysis and octagons.

We discuss some implementation issues, and we compare it with similar tools, showing how our tool achieves a higher level of automation and precision while having comparable performances.

PDF file

In  Proceedings of the 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'07)

Publisher  Springer Verlag
All copyrights reserved by Springer 2007.

Details