Static analysis

Static analysis is the act of deriving information about computer software (or, more generally, hardware or protocols) without actually running it, as opposed to dynamic analysis, which basically means testing the software by running it on sample cases in the hope of exercising a bug.

Certain commercial providers call “static analysis” any check based on the source code of the program, including stylistic checks (e.g. presence of comments at any function entry, statistics on loop nests, and so on). In contrast, the analysis that we do inside the STATOR project is sound and based on the semantics of the program — meaning that if the analysis tool concludes, for instance, that some type conversion cannot overflow because the range of the value does not exceed that of the target type, this this is true for all execution of the program. “Sound” means that our analysis will never ignore some cases that are actually possible in the program, so if it says that some problem does not occur, then it cannot occur (in some sense, it has proved that it cannot occur). Many commercial tools will instead provide false negatives — failing to point some issue that the tool is claimed to detect.

This sounds too good to be true, and you may think there should be a catch. There are actually several. The main one is that a tool cannot be both sound and complete — here, completeness means that the tool is capable of proving any true property of the program. This means that a sound tool will fail to prove some properties, thus issuing warnings about problems that do not exist in the real system — false positives or false alarms. This is unavoidable, as it is a consequence of mathematical properties of computable functions (the mathematical constructs underlying computer programs), more precisely of Rice's theorem.