Paper Info
Title
Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs
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.
Year
DOI
Venue
2004
10.1007/978-3-540-27815-3_22
ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY: PROCEEDINGS
Keywords
Field
DocType
operational semantics
Operational semantics,Programming language,Functional approach,Computer science,Abstract interpretation,Proof theory,Imperative programming,Theoretical computer science,Program analysis,Software development,Semantics
Conference
Volume
ISSN
Citations 
3116
0302-9743
15
PageRank 
References 
Authors
0.89
25
2
Name
Order
Citations
PageRank
Bertrand Jeannet164129.06
Wendelin Serwe241122.55