Static program analysis: Difference between revisions

Revision as of 19:43, 6 November 2004

Revision as of 12:21, 28 December 2004

Line 10:

'''Static analysis''' is a family of [[formal method]]s for automatically deriving information about the behavior of computer [[software]] (and also [[hardware]]). One possible application of static analysis is automated [[debugging]] aid, especially the finding of run-time errors -- roughly speaking, events causing program [[crash]]es.

Briefly, program analysis — including finding possible run-time errors -- is [[undecidable]]: there's is no mechanical method that can always answer truthfully whether programs may or not exhibit runtime errors. This is a mathematically founded result dating from the works of [[Alonzo Church|Church]], [[Kurt Gödel|Gödel]] and [[Alan Turing|Turing]] in the [[1930s]] (see [[halting problem]] and [[Rice's theorem]]).

There exist two main families of formal static analysis:

Line 28:

*[[Crash-only software]]

*[[Graceful degradation]]

==External links==