PostScript
Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs
Bertrand Jeannet and Wendelin Serwe
Proceedings of the 10th International Conference on Algebraic Methodology and
Software Technology AMAST'2004 (Stirling, UK), July 2004
Preliminary version (with extensions) available as INRIA Research Report RR-4904.
Abstract:
We propose a new approach to interprocedural analysis and verification, consisting of deriving an interprocedural analysis method by abstract interpretation of the standard operational semantics of programs. The advantages of this approach are twofold. From a methodological point of view, it provides a direct connection between the concrete semantics of the program and the effective analysis, which facilitates implementation and correctness proofs. This method also integrates two main, distinct methods for interprocedural analysis, namely the call-string and the functional approaches introduced by Sharir and Pnueli. This enables strictly more precise analyses and additional flexibility in the tradeoff between efficiency and precision of the analysis.
| AMAST paper (15 pages) | |
PostScript |
| INRIA Research Report (54 pages) | |
PostScript |