Using Graph Transformations and Graph Abstractions for Software Verification

Eduardo Zambon

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    71 Downloads (Pure)

    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 languageUndefined
    Title of host publicationFifth International Conference on Graph Transformations (ICGT 2010)
    EditorsHartmut Ehrig, Arend Rensink, Grzegorz Rozenberg, Andy Schurr
    Place of PublicationBerlin
    PublisherSpringer
    Pages416-418
    Number of pages3
    ISBN (Print)978-3-642-15927-5
    DOIs
    Publication statusPublished - Jul 2010

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume6372
    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