de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Privacy Policy Disclaimer Contact us
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Conference Paper

Description Logics for Shape Analysis

MPS-Authors
http://pubman.mpdl.mpg.de/cone/persons/resource/persons44487

Georgieva,  Lilia
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons44970

Maier,  Patrick
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons44099

Beckert,  Bernhard
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

Georgieva, L., & Maier, P. (2005). Description Logics for Shape Analysis. In Third IEEE International Conference on Software Engineering and Formal Methods (SEFM 2005) (pp. 321-330). Los Alamitos, USA: IEEE.


Cite as: http://hdl.handle.net/11858/00-001M-0000-000F-2633-A
Abstract
Verification of programs requires reasoning about sets of program states. In case of programs manipulating pointers, program states are pointer graphs. Verification of such programs involves reasoning about unbounded sets of graphs. Three-valued shape analysis (Sagiv et. al.) is an approach based on explicit manipulation of 3-valued shape graphs, which abstract sets of pointer graphs. Other approaches use symbolic representations, e.g. by describing (sets of) graphs as logical formulas. Unfortunately, many resulting logics are either undecidable or cannot express crucial properties like reachability and separation. In this paper, we investigate an alternative approach. We study well-known description logics as a framework for symbolic shape analysis. We propose a predicate abstraction based shape analysis, parameterized by description logics to represent the abstraction predicates. Depending on the particular logic chosen sharing, reachability and separation in pointer data structures are expressible.