Safe Pointers by Graph Transformation

From The Programming Languages and Systems Research Group
Jump to: navigation, search

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.

Further Information