Abstract interpretation: Achievements and perspectives
Patrick M. Cousot · 2000
Computerized modern societies are highly fragile to software bugs. Traditional testing methods hardly scale up for large safety critical systems as found in avionics, automotive, healthcare, e-commerce and security industry. As a viable alternative, static analysis consists in determining and verifying statically dynamic properties of programs. This is completely automatic (since programs are not actually executed) and covers all possible cases (as opposed to testing). This approach has had significant success stories and its industrialization recently started. Since the program total verification problem is undecidable, the key idea is that interpretation. The scope of application of abstract interpretation ranges from the theoretical design of hierarchies of the semantics of programming languages to the practical design of generic program static analyzers.