Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs

Bertrand Jeannet 1 Wendelin Serwe 2
2 Lande - Logiciel : ANalyse et DEveloppement
IRISA - Institut de Recherche en Informatique et Systèmes Aléatoires, Inria Rennes – Bretagne Atlantique
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.
Document type :
Reports
Complete list of metadatas

https://hal.inria.fr/inria-00071678
Contributor : Rapport de Recherche Inria <>
Submitted on : Tuesday, May 23, 2006 - 6:30:47 PM
Last modification on : Friday, November 16, 2018 - 1:22:19 AM
Long-term archiving on : Sunday, April 4, 2010 - 10:32:53 PM

Identifiers

  • HAL Id : inria-00071678, version 1

Citation

Bertrand Jeannet, Wendelin Serwe. Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs. [Research Report] RR-4904, INRIA. 2003. ⟨inria-00071678⟩

Share

Metrics

Record views

187

Files downloads

652