### Abstract

In this abstract we present an overview of our intended approach for the verification of software written in imperative programming languages. This approach is based on model checking of graph transition systems (GTS), where each program state is modeled as a graph and the exploration engine is specified by graph transformation rules. We believe that graph transformation [13] is a very suitable technique to model the execution semantics of languages with dynamic memory allocation. Furthermore, such representation provides a clean setting to investigate the use of graph abstractions, which can mitigate the space state explosion problem that is inherent to model checking techniques.

Original language | Undefined |
---|---|

Title of host publication | Fifth International Conference on Graph Transformations (ICGT 2010) |

Editors | Hartmut Ehrig, Arend Rensink, Grzegorz Rozenberg, Andy Schurr |

Place of Publication | Berlin |

Publisher | Springer |

Pages | 416-418 |

Number of pages | 3 |

ISBN (Print) | 978-3-642-15927-5 |

DOIs | |

Publication status | Published - Jul 2010 |

### Publication series

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

Publisher | Springer Verlag |

Volume | 6372 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

### Keywords

- IR-73569
- METIS-271047
- Graph Abstraction
- Graph Transformation
- Software Verification
- EWI-18526

## Cite this

Zambon, E. (2010). Using Graph Transformations and Graph Abstractions for Software Verification. In H. Ehrig, A. Rensink, G. Rozenberg, & A. Schurr (Eds.),

*Fifth International Conference on Graph Transformations (ICGT 2010)*(pp. 416-418). (Lecture Notes in Computer Science; Vol. 6372). Berlin: Springer. https://doi.org/10.1007/978-3-642-15928-2_37