Static analysis

Revision as of 21:10, 25 October 2012 by David Monniaux (talk | contribs)
Jump to navigation Jump to search

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.