An example is the trace semantics of a programming language. The semantics of programs in the language describes all possible program executions as a set of traces over states chosen in a given set of possible states. Two successive states in a trace correspond to an elementary program computation step. An example of a property is the termination property stating that all execution traces should be finite.

Formal verification methods are very hard to put in practice because both the semantics and the specification of a complex system are extremely difficult to define. Even when this is possible, the proof cannot be automated (using a theorem prover, a model checker, or a static analyzer) without great computational costs. Considering all possible systems is even harder. Hence it is necessary either to work in the small (for example, model checking) or to consider approximations of large systems (for example, abstract model checking).

Abstract Interpretation. Abstract interpretation⁵ is a theory of sound approximation of mathematical structures, in particular those involved in the description of the behavior of computer systems. To prove a property, the abstraction idea is to consider a sound overapproximation of the collecting semantics, a sound underapproxima-tion of the property to be proven, and to make the correctness proof in the abstract.

For automated proofs, these abstractions must be computer-representable, so they are not chosen in the mathematical concrete domain but in an abstract domain. The correspondence is given by a concretization function mapping abstract properties to corresponding concrete properties. Formal verification being undecidable, the abstraction may be incomplete—that is, it produces false alarms, a case when a concrete property holds but this cannot be proved in the abstract for the given abstraction, which must therefore be refined. The abstraction function is the inverse of the concretization function. It maps concrete properties to their approximation in the abstract domain. Applied to the collecting semantics of a computer system, it formally provides an abstraction of the properties of the system. Abstract verification methods consist of designing an abstraction function that is coarse

michael JacKson
Development
of the formal
model is, above
all, an engineering
task. in the
established
engineering
branches, the
challenge is met
by experience
accumulated in
each particular
product class
and captured
in a normal
design discipline.

enough so that the abstract collecting semantics is computer-representable and effectively computable and is precise enough so that the abstract-col-lecting semantics implies the specification.

Abstract interpretation formalizes the intuition about abstraction. It allows the systematic derivation of sound reasoning methods and effective algorithms for approximating undecidable or highly complex problems in various areas of computer science (semantics, verification and proof, model checking, static analysis, program transformation and optimization, typing, or software steganography). Its main current application is on the safety and security of complex hardware and software computer systems.

Verification by Static Analysis. Static code analysis is the fully automatic analysis of a computer system by direct inspection of the source or object code describing the system with respect to the semantics of the code (without executing programs, as in dynamic analysis). The proof is done in the abstract by effectively computing an abstraction of the collecting semantics of the system. Examples of successful static analyzers used in an industrial context are aiT ( www.absint.com/ait used to compute an overapproximation of the worst-case execution time⁸) and Astrée ( www.astree.ens.fr used to compute an overapproximation of the collecting semantics to prove the absence of runtime errors⁶).

Their growing success is a result of their being useful (such as, they tackle practical problems), sound (their results can be trusted), nonintrusive (end users do not have to alter their programming methods (for example, by producing the specification and abstract semantics that can be directly derived from the program text), realistic (applicable in any weird industrial environment), scalable (to millions of lines of code as found in actual industrial code), and conclusive (producing few or no false alarms).

The design of language-based semantics and abstractions is extremely difficult but possible on a well-defined family of programs (for example, synchronous, time-triggered, real-time, safety-critical, embedded software written or automatically generated in C for