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. © 2010 Springer-Verlag.
CITATION STYLE
Zambon, E. (2010). Using graph transformations and graph abstractions for software verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6372 LNCS, pp. 416–418). https://doi.org/10.1007/978-3-642-15928-2_37
Mendeley helps you to discover research relevant for your work.