Safe Pointers by Graph Transformation
The aim of the Safe Pointers by Graph Transformation (SPGT) project is to develop tools to statically check the shape properties of data structures. We hope to achieve this by modelling data-structure manipulations as graph-transformation rules.
Several tools for SPGT have been implemented. Adam Bakewell has implemented the checking algorithm as a command-line tool.
GRS checking has been embedded into C by Mike Dodds, in a language called C-GRS. Further information about C-GRS is available in the following publications:
- Mike Dodds and Detlef Plump. Extending C for checking shape safety (.pdf). In Proc. Graph Transformation for Verification and Concurrency (GT-VC 2005), volume 154(2) of Electronic Notes in Theoretical Computer Science. Elsevier, 2006.
- Mike Dodds. Graph Transformation and Pointer Structures (.pdf). PhD thesis, The University of York, 2008.
- Safe Pointers by Graph Transformation - Adam Bakewell's page on the SPGT project