B. Jeannet, W. Serwe. Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs. In Int.\ Conf.\ on Algebraic Methodology and Software Technology, AMAST'04, LNCS, Volume 3116, July 2004.
Download paper:
Adobe portable document (pdf)
Copyright notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.
We propose a new approach to interprocedural analysis/verification, consisting in 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 correction 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
Bertrand Jeannet http://pop-art.inrialpes.fr/people/bjeannet/
@InProceedings{amast04,
Author = {Jeannet, B. and Serwe, W.},
Title = {Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs},
BookTitle = {Int.\ Conf.\ on Algebraic Methodology and Software Technology, AMAST'04},
Volume = { 3116},
Series = {LNCS},
Month = {July},
Year = {2004}
}
Get EndNote Reference (.ref)