Static program analysis: Difference between revisions

Revision as of 16:06, 1 March 2021

Revision as of 16:21, 1 March 2021

Line 43:

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> The [[Frama-C]] value analysis plugin, [[Polyspace]], and [[Astrée]] heavily rely on abstract interpretation.

* [[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]]) ).