We describe our software tool Julia for the static analysis of full Java bytecode, for optimisation as well as verification. This tool is generic since abstract domains (analyses) are not part of Julia but rather external classes that specialise its behaviour. Static analysis is performed through a denotational or constraint-based fixpoint calculation, focused on some program points called watchpoints. These points specify where the result of the analysis is useful, and can be automatically placed by the abstract domain or manually provided by the user. Julia can be instructed to include a given set of library Java classes in the analysis, in order to improve its precision. Moreover, it gives abstract domains the opportunity to approximate control and data-flow arising from exceptions and subroutines.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.