Static Analyzer for Java — Apron + Soot
Java bytecode verifier using abstract interpretation. Soot for IR and control-flow graphs, Apron for numerical abstract domains.
Static analyzer for Java bytecode using abstract interpretation. Soot parses class files into the Jimple IR. Its control-flow graph drives a worklist algorithm. Apron supplies the numerical abstract domains (intervals, polyhedra) for tracking value ranges and reasoning about overflow. The analyzer checks user-specified properties like “does this assertion always hold” or “can this null pointer ever be dereferenced” and returns yes, no, or unknown.
Java, Maven, Docker, GitLab CI. ETH Zurich Rigorous Software Engineering.