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.
|Published in||Proceedings of the 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'07)|
All copyrights reserved by Springer 2007.