### Abstract

Automatic verification of imperative programs that destructively manipulate heap data structures is challenging. In this paper we propose an approach for verifying that such programs do not corrupt their data structures. We specify heap data structures such as lists, arrays of lists, and trees inductively as solutions of logic programs. We use off-the-shelf first-order theorem provers to reason about these specifications.

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

Title of host publication | Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09) |

Editors | Nicolas Peltier, Viorica Sofronie-Stokkermans |

Place of Publication | Oslo |

Publisher | University of Oslo |

Pages | 75-89 |

Number of pages | 15 |

ISBN (Print) | 82-7368-347-8 |

Publication status | Published - Jul 2009 |

Event | International Workshop on First-Order Theorem Proving, FTP 2009 - Oslo, Norway Duration: 6 Jul 2009 → 7 Nov 2012 |

### Conference

Conference | International Workshop on First-Order Theorem Proving, FTP 2009 |
---|---|

Country | Norway |

City | Oslo |

Period | 6/07/09 → 7/11/12 |

## Fingerprint Dive into the research topics of 'Inductive reasoning for shape invariants'. Together they form a unique fingerprint.

## Cite this

Georgieva, L., & Maier, P. (2009). Inductive reasoning for shape invariants. In N. Peltier, & V. Sofronie-Stokkermans (Eds.),

*Proceedings of the 7th International Workshop on First-Order Theorem Proving (FTP'09)*(pp. 75-89). University of Oslo. http://ceur-ws.org/Vol-556/paper08.pdf