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

Francesco Logozzo

Abstract

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.

Details

Publication typeInproceedings
Published inProceedings of the 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'07)
Volume4349
PublisherSpringer Verlag
> Publications > An abstract interpretation-based static analyzer for modular analysis and verification of Java classes