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). 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) 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 or may be reduced to finite state by abstraction; Symbolic execution, as used to derive mathematical expressions representing the value of mutated variables at particular points in the code. Data-driven static analysis Data-driven static analysis uses large amounts of code to infer coding rules. For instance, one can use all Java open-source packages on GitHub to learn a good analysis strategy. The rule inference can use machine learning techniques. It is also possible to learn from a large amount of past fixes and warnings. Remediation Static analyzers produce warnings. For certain types of warnings, it is possible to design and implement automated remediation techniques. For example, Logozzo and Ball have proposed automated remediations for C# cccheck. See also References Further reading "Abstract interpretation and static analysis," International Winter School on Semantics and Applications 2003, by David A. Schmidt Program analysis Software engineering