Static program analysis: Difference between revisions

Revision as of 15:47, 4 September 2004

Revision as of 19:20, 6 September 2004

Line 8:

'''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: