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

PDF
254kB 
Abstract:  Abstract. Graphs are an intuitive model for states of a (software) system that include pointer structures — for instance, objectoriented 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 firstorder 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 subfragment 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