Safe Pointers by Graph Transformation
From The Programming Languages and Systems Research Group
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.
Implementations
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.
Further Information
- Safe Pointers by Graph Transformation - Adam Bakewell's page on the SPGT project
