Static analysis

Static analysis is the examination of program code without executing it, with the goal of discovering properties that hold for all possible inputs — or finding bugs that would manifest on some input. Unlike dynamic testing, which samples behavior by running the program on specific inputs, static analysis reasons about all possible behaviors simultaneously. It is the computational analog of proof: instead of checking that a bridge holds under test loads, it calculates that the bridge will hold under any load within the design parameters.

The foundational technique is abstract interpretation, developed by Patrick and Radhia Cousot, which computes sound over-approximations of program behavior by evaluating the program on abstract domains rather than concrete values. An abstract domain trades precision for tractability: instead of tracking the exact integer value of a variable, it might track only whether the variable is positive, negative, or zero. The analysis is conservative — it may report false positives (claiming a bug exists when it does not) but never false negatives (missing a real bug). This conservatism makes static analysis a tool for assurance, not merely for debugging.

Modern static analysis ranges from lightweight tools that find null pointer dereferences and buffer overflows in millions of lines of code, to heavyweight verifiers that establish functional correctness of critical systems. Type systems are a form of static analysis — perhaps the most successful in history — catching category errors at compile time before they become runtime failures. Model checkers verify protocol-level properties by exhaustive state-space exploration. SMT solvers discharge proof obligations by combining SAT search with theory-specific reasoning. Each of these tools occupies a different point on the spectrum of precision, scalability, and automation.

The practical adoption of static analysis has been uneven. It is standard in safety-critical domains — aviation, medical devices, automotive — where certification standards require evidence beyond testing. But it remains marginal in mainstream software development, where the culture of move