An abstract interpretation-based static analyzer for modular analysis and verification of Java classes

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.

vmcai07.pdf
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

TypeInproceedings
Volume4349
> Publications > An abstract interpretation-based static analyzer for modular analysis and verification of Java classes