Description logics for shape analysis

Lilia Georgieva, Patrick Maier

Research output: Chapter in Book/Report/Conference proceedingConference contribution

6 Citations (Scopus)

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.
Original languageEnglish
Title of host publication3rd IEEE International Conference on Software Engineering and Formal Methods
Subtitle of host publicationSEFM 2005; Koblenz, Germany, September 7-9, 2005; Proceedings
PublisherIEEE
Pages321-330
Number of pages10
DOIs
Publication statusPublished - Sep 2005
Event3rd IEEE International Conference on Software Engineering and Formal Methods - Koblenz, Germany
Duration: 7 Sep 20059 Sep 2005

Conference

Conference3rd IEEE International Conference on Software Engineering and Formal Methods
CountryGermany
CityKoblenz
Period7/09/059/09/05

Keywords

  • description logics
  • shape analysis
  • program analysis
  • pointer programs

Fingerprint Dive into the research topics of 'Description logics for shape analysis'. Together they form a unique fingerprint.

  • Cite this

    Georgieva, L., & Maier, P. (2005). Description logics for shape analysis. In 3rd IEEE International Conference on Software Engineering and Formal Methods: SEFM 2005; Koblenz, Germany, September 7-9, 2005; Proceedings (pp. 321-330). IEEE. https://doi.org/10.1109/SEFM.2005.16