Using Graph Transformations and Graph Abstractions for Software Verification

Eduardo Zambon

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

    191 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
    EventFifth International Conference on Graph Transformations, ICGT 2010 - Enschede, The Netherlands
    Duration: 27 Sept 20102 Oct 2010

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    Volume6372
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    ConferenceFifth International Conference on Graph Transformations, ICGT 2010
    Period27/09/102/10/10
    Other27 Sep - 02 Oct 2010

    Keywords

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

    Cite this