Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
On the Relative Completeness of Bytecode Analysis versus Source Code Analysis

Francesco Logozzo and Manuel Fähndrich


We discuss the challenges faced by bytecode analyzers designed for code verification compared to similar analyzers for source code. While a bytecode-level analysis brings many simplifications, eg, fewer cases, independence from source syntax, name resolution, etc., it also introduces precision loss that must be recovered either via preprocessing, more precise abstract domains, more precise transfer functions, or a combination thereof.

The paper studies the relative completeness of a static analysis for bytecode compared to the analysis of the program source. We illustrate it through examples originating from the design and the implementation of Clousot, a generic static analyzer based on Abstract Interpretation for the analysis of MSIL.


Publication typeInproceedings
Published inProceedings of the International Conference on Compiler Construction
PublisherSpringer Verlag

Newer versions

Francesco Logozzo. Our Experience with the CodeContracts Static Checker, Springer, January 2012.

Francesco Logozzo. Practical verification for the working programmer with CodeContracts and Abstract Interpretation - Invited Talk, Springer Verlag, January 2011.

Manuel Fahndrich and Francesco Logozzo. Static contract checking with Abstract Interpretation, Springer Verlag, October 2010.

> Publications > On the Relative Completeness of Bytecode Analysis versus Source Code Analysis