## Abstract

We present a new algorithm for checking the shape-safety of pointer manipulation programs. In our model, an abstract, data-less pointer structure is a graph. A shape is a language of graphs. A pointer manipulation program is modelled abstractly as a set of graph rewrite rules over such graphs where each rule corresponds to a pointer manipulation step. Each rule is annotated with the intended shape of its domain and range and our algorithm checks these annotations.

We formally define the algorithm and apply it to a binary search tree insertion program. Shape-safety is undecidable in general, but our method is more widely applicable than previous checkers, in particular, it can check programs that temporarily violate a shape by the introduction of intermediate shape definitions.

Original language | English |
---|---|

Title of host publication | Relational Methods in Computer Science (RelMiCS 7), Revised Selected Papers |

Editors | R Berghammer, B Moller, G Struth |

Place of Publication | Berlin |

Publisher | Springer |

Pages | 48-61 |

Number of pages | 14 |

ISBN (Print) | 3-540-22145-X |

DOIs | |

Publication status | Published - 2004 |

Event | 7th International Seminar on Relational Methods in Computer Science/2nd International Workshop on Applications of Kleene Algebra - Bad Malente Duration: 12 May 2003 → 17 May 2003 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Publisher | Springer |

Volume | 3051 |

### Conference

Conference | 7th International Seminar on Relational Methods in Computer Science/2nd International Workshop on Applications of Kleene Algebra |
---|---|

City | Bad Malente |

Period | 12/05/03 → 17/05/03 |