Home | deutsch  | Legals | Sitemap | KIT

Abstract Interpretation of Symbolic Execution with Explicit State Updates

Abstract Interpretation of Symbolic Execution with Explicit State Updates
Author(s):

Richard Bubel
Reiner Hähnle
Benjamin Weiß

Links:
Source:

7th International Symposium on Formal Methods for Components and Objects (FMCO 2008), Sophia Antipolis, France. LNCS 5751, Springer, 2009

Systems for deductive software verification model the semantics of their target programming language with full precision. On the other hand, abstraction based approaches work with approximations of the semantics in order to be fully automatic. In this paper we aim at providing a uniform framework for both fully precise and approximate reasoning about programs. We present a sound dynamic logic calculus that integrates abstraction in the sense of abstract interpretation theory. In the second part of the paper, we apply the approach to the analysis of secure information flow.

BibTeX

@inproceedings{BubelEtAl2009,
  author       = {Richard Bubel and Reiner H{\"a}hnle and Benjamin Wei{\ss}},
  title        = {Abstract Interpretation of Symbolic Execution with Explicit State Updates},
  editor       = {Frank S. de Boer and Marcello M. Bonsangue and Eric Madeleine},
  booktitle    = {Revised Lectures, 7th International Symposium on Formal Methods for Components and Objects (FMCO 2008)},
  volume       = {5751},
  series       = {LNCS},
  pages        = {247--277},
  publisher    = {Springer},
  year         = {2009}
}