Canonical Graph Shapes

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 logic (LSL) 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.