Static program analysis

Static analysis is the term applied to the analysis of computer software that is performed without actually executing programs built from that software (analysis performed on executing programs is known as dynamic analysis). In most cases the analysis is performed on some version of the source code and in the other cases some form of the object code. The term is usually applied to the analysis performed by an automated tool, with human analysis being called program understanding or program comprehension.

The sophistication of the analysis performed by tools varies from those that only consider the behavior of individual statements and declarations, to those that include the complete source code of a program in their analysis. Uses of the information obtained from the analysis vary from highlighting possible coding errors (e.g., the lint tool) to formal methods that mathematically prove properties about a given program (e.g., its behavior matches that of its specification).

Some people consider software metrics to be a form of static analysis.

A growing commercial use of static analysis is in the verification of properties of software used in safety-critical computer systems.

Formal methods

Formal methods is the term applied to the analysis of software (and hardware) whose results are obtained purely through the use of rigorous mathematical methods. The mathematical techniques used include denotational semantics, axiomatic semantics, operational semantics, and abstract interpretation.

It has been proved that finding possible run-time errors – is undecidable: there is no mechanical method that can always answer truthfully whether programs may or not exhibit runtime errors. This result dates from the works of Church, Gödel and Turing in the 1930s (see the halting problem and Rice's theorem). As with most undecidable questions, one can still attempt to give useful approximate solutions.

Some of the implementation techniques of formal static analysis include:

• model checking considers systems that have finite state or may be reduced to finite state by abstraction;
• abstract interpretation models the effect that every statement has on the state of an abstract machine (ie, it 'executes' [[Media:Media:Example.ogg[[Media:Media:Example.ogg[[Media:Media:Example.ogg[[Media:Media:Example.ogg]]]]]]]]the software based on the mathematical properties of each statement and declaration).

See also

• DAEDALUS
• Formal semantics of programming languages
• Formal verification
• Software analysis
• Software testing
• Crash-only software
• Graceful degradation
• SPARK programming language
• List of tools for static code analysis

External links

• Page of external links to static analysis tools
• Information of software management
• Citations from CiteSeer
• ASTRÉE project, with explanations on static analysis by abstract interpretation
• PREfix from Microsoft Research team - not on GA (General availability) yet.
• Type Inference and Static Analysis for Object-Oriented Software by Jens Palsberg
• Securing Web Application Code by Static Analysis and Runtime Protection