The Checker Framework:
a framework to build pluggable type systems for Java, allowing you to enforce and infer advanced program properties.
Example uses include enforcing freedom from null-pointer exceptions and verifying information flow in Android apps.
Correlated calls:
a tool for improving the precision of static data-flow analysis for object-oriented programs;
comes with an implementation of the IDE algorithm
Flix: a declarative programming language for fixpoints on lattices.
μC++:
C++ extended with high-performance concurrency.