Editing Static program analysis (section)

== Formal methods ==

{{main|Formal methods}}

Formal methods is the term applied to the analysis of [[software]] (and [[computer 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]].

By a straightforward reduction to the [[halting problem]], it is possible to prove that (for any [[Turing complete]] language), finding all possible run-time errors in an arbitrary program (or more generally any kind of violation of a specification on the final result of a program) is [[decision problem|undecidable]]: there is no mechanical method that can always answer truthfully whether an arbitrary program may or may not exhibit runtime errors. This result dates 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]]). As with many undecidable questions, one can still attempt to give useful approximate solutions.

Some of the implementation techniques of formal static analysis include:<ref>{{cite web|title=A Survey of Automated Techniques for Formal Software Verification|author=Vijay D’Silva|publisher=Transactions On CAD|date=2008|url=http://www.kroening.com/papers/tcad-sw-2008.pdf|access-date=2015-05-11|display-authors=etal|url-status=live|archive-url=https://web.archive.org/web/20160304074248/http://www.kroening.com/papers/tcad-sw-2008.pdf|archive-date=2016-03-04}}</ref>
* [[Abstract interpretation]], to model the effect that every statement has on the state of an abstract machine (i.e., it 'executes' the software based on the mathematical properties of each statement and declaration). This abstract machine over-approximates the behaviours of the system: the abstract system is thus made simpler to analyze, at the expense of ''incompleteness'' (not every property true of the original system is true of the abstract system). If properly done, though, abstract interpretation is ''sound'' (every property true of the abstract system can be mapped to a true property of the original system).<ref>{{cite web | title=A Formal Methods-based verification approach to medical device software analysis |last=Jones |first=Paul |publisher=Embedded Systems Design |date=2010-02-09 |url=http://embeddeddsp.embedded.com/design/opensource/222700533 |access-date=2010-09-09 |url-status=dead |archive-url=https://web.archive.org/web/20110710185427/http://embeddeddsp.embedded.com/design/opensource/222700533 |archive-date=July 10, 2011 }}</ref>
* [[Data flow analysis|Data-flow analysis]], a lattice-based technique for gathering information about the possible set of values;
* [[Hoare logic]], a [[formal system]] with a set of logical rules for reasoning rigorously about the [[correctness of computer programs]]. There is tool support for some programming languages (e.g., the [[SPARK programming language]] (a subset of [[Ada (programming language)|Ada]]) and the [[Java Modeling Language]]—JML—using [[ESC/Java]] and [[ESC/Java2]], Frama-C WP ([[weakest precondition]]) plugin for the C language extended with ACSL ([[ANSI/ISO C Specification Language]]) ).
* [[Model checking]], considers systems that have [[finite-state machine|finite state]] or may be reduced to finite state by [[abstraction (computer science)|abstraction]];
* [[Symbolic execution]], as used to derive mathematical expressions representing the value of mutated variables at particular points in the code.
* [[Nullable]] reference analysis