The Julia Static Analyzer for Java']Java

The Julia static analyzer applies abstract interpretation to the analysis and verification of Java bytecode. It is the result of 13 years of engineering effort based on theoretical research on denotational and constraint-based static analysis through abstract interpretation. Julia is a library for static analysis, over which many checkers have been built, that verify the absence of a large set of typical errors of software: among them are null-pointer accesses, non-termination, wrong synchronization and injection threats to security. This article recaps the history of Julia, describes the technology under the hood of the tool, reports lessons learned from the market, current limitations and future work.