PI-1543: Abstracting Call-Stacks for Interprocedural Verification
of Imperative Programs
Bertrand Jeannet, Wendelin Serwe
http://www.irisa.fr/bibli/publi/pi/2003/1543/1543.html
50 pages - juin 2003

Abstract
We address in this paper the verification of imperative programs with
recursion. Our approach consists in using abstract interpretation to
relate the standard semantics of imperative programs to an abstract
semantics, by the mean of a Galois connection, and then to resort to
intraprocedural techniques, which can be applied on the abstract
semantics. This approach allows the reuse of classical intraprocedural
techniques with few modifications, generalises existing approaches to
interprocedural analysis and offers additional flexibility, as it keeps
substantial information on the call-stack of the analysed program.

Résumé
Nous nous intéressons à la vérification de programmes impératifs
récursifs. Notre approche consiste à utiliser le cadre théorique de
l'interprétation abstraite pour relier la sémantique standard des
programmes impératifs à une sémantique abstraite, au moyen d'une
connexion de Galois, puis de recourir à des techniques d'analyse
intraprocédurale qui peuvent être directement appliquée à la sémantique
abstraite. Cette approche permet de réutiliser des techniques
interprocédurales classiques avec peu de modifications, généralise des
méthodes existantes pour l'analyse interprocédurale, et offre une
souplesse accrue en maintenant des informations précises sur la pile
d'appel du programme analysé.

Keywords: Interprocedural verification, abstract interpretation

Mots clefs: Vérification interprocédurale, interprétation abstraite