The first application is to predicate abstraction that we generalize to obtain generic abstractions which are parameterized and so can be adapted to particular programs as opposed to classical predicate abstraction which is specialized for a single program.
The second application is to the analysis of critical embedded avionic software to verify the absence of runtime errors and good usage of C.
We argue that such results cannot be obtained by classical predicate abstraction with refinement.
\bibitem{CousotVerona04}
P{.} Cousot.
\newblock Verification by Abstract Interpretation.
\newblock Seminario, Dipartimento di Informatica, Universit{\`a} degli Studi di Verona,
Verona, Italy. September 2nd, 2004.
@conference{{CousotVerona04,
author = {P{.} Cousot},
title = {Verification by Abstract Interpretation},
booktitle = {Seminario},
address = {Dipartimento di Informatica, Universit{\`a} degli Studi di Verona,
Verona, Italy},
month = {September 2nd},
year = 2004,
}