Abstract interpretation is a formal method that enables the static determination (i.e. at compile-time) of the dynamic properties (i.e. at run-time) of programs. Up to now, this method has been applied to fairly simple languages (first-order imperative, functional, logic or parallel languages). However, modern programming languages such as Modula-3 or even older ones such as Pascal offer powerful and complex programming mechanisms (call-by-reference, local procedures passed as parameters, non-local gotos, exceptions) that greatly increase their expressiveness and semantic complexity. This thesis is concerned with the abstract interpretation of higher-order imperative languages. In the first part, we show that a too "naive" application of abstract interpretation to such higher-order languages is extremely costly and unprecise. We then define a new semantics of higher-order imperative languages that is better suited to abstract interpretation and establish its semantic correctness for a new undecidable class of programs which, in particular, contains the class of all Pascal programs, for which membership is decidable. Then, in the second part, we introduce the abstract debugging of higher-order imperative programs which is a method that enables the compile-time and formal debugging of programs and we present the Syntox system which enables the abstract debugging of Pascal programs by computing the value range of the scalar variables of a program.
[PostScript, PDF, Software]