Canonical Graph Shapes

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    43 Citations (Scopus)


    Graphs are an intuitive model for states of a (software) system that include pointer structures | for instance, object-oriented programs. However, a naive encoding results in large individual states and large, or even unbounded, state spaces. As usual, some form of abstraction is necessary in order to arrive at a tractable model. In this paper we propose a decidable fragment of first-order graph logic that we call local shape logicLSL as a possible abstraction mechanism, inspired by previous work of Sagiv, Reps and Wilhelm. An LSL formula constrains the multiplicities of nodes and edges in state graphs; abstraction is achieved by reasoning not about individual, concrete state graphs but about their characteristic shape properties. We go on to define the concept of the canonical shape of a state graph, which is expressed in a monomorphic sub-fragment of LSL, for which we define a graphical representation. We show that the canonical shapes give rise to an automatic finite abstraction of the state space of a software system, and we give an upper bound to the size of this abstract state space.
    Original languageEnglish
    Title of host publicationProgramming Languages and Systems
    Subtitle of host publication13th European Symposium on Programming, ESOP 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29-April 2, 2004. Proceedings
    EditorsDavid Schmidt
    Place of PublicationBerlin
    Number of pages15
    ISBN (Print)3-540-21313-9
    Publication statusPublished - 2004
    Event13th European Symposium On Programming, ESOP 2004 - Barcelona, Spain
    Duration: 29 Mar 20042 Apr 2004
    Conference number: 13

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    Conference13th European Symposium On Programming, ESOP 2004
    Abbreviated titleESOP


    • EWI-6925
    • IR-66356


    Dive into the research topics of 'Canonical Graph Shapes'. Together they form a unique fingerprint.

    Cite this