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  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.
|Name||Lecture Notes in Computer Science|
|Conference||Fifth International Conference on Graph Transformations, ICGT 2010|
|Period||27/09/10 → 2/10/10|
|Other||27 Sep - 02 Oct 2010|
- Graph Abstraction
- Graph Transformation
- Software Verification