static analyzers check statically very simple properties
of software. Roughly speaking, they mostly look for predefined patterns
in the source code usually relying on the abstract syntax tree
of the program. If a piece of code falls into one of this patterns, then it is reported to the user, as this is a signal that it might be a bug.
For instance, a Sonarqube rule detects that “Identical expressions should not be used on both sides of a binary operator”. So, if we have an expression like a==a then the Sonarqube’s rule will raise a warning. Instead, it would not raise a warning for a+0==0+a, since these two expressions are not identical but their execution leads exactly to the same results.
Instead, semantic static analyzers focus on the meaning of the program. Since we cannot run a program on all possible executions and environment conditions, these tools build up an abstract representation of the states of the program, and perform a static simulation of their execution. For instance, instead of considering all the possible numerical values of an integer input, they approximate this with the sign or the interval of the possible numerical values. In the example above, a simple symbolic propagation would be able to discover that a+0 is always equal to 0+a, and therefore raise a warning on this comparison. It is possible to build up sound static analyzers by proving well-defined mathematical theorems on the formalization of the analysis applied by the tool.
Julia is the only commercial tool that can claim this soundness on Java and Android programs. The robustness of Julia’s approach has been recognized by the scientific community through the publication of several scientific articles. This result was possible thanks to the rigorous approach applied by Julia and supervised by our internal scientific committee