Canonical Graph Shapes


Share/Save/Bookmark

Rensink, A. (2004) Canonical Graph Shapes. In: Programming Languages and Systems (ESOP).

[img]
Preview
PDF
248Kb
Abstract:Abstract. 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.
Item Type:Conference or Workshop Item
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/66356
Official URL:http://dx.doi.org/10.1007/b96702
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page