Using Graph Transformations and Graph Abstractions for Software Verification

Eduardo Zambon, Arend Rensink

    Research output: Book/ReportReportProfessional

    73 Downloads (Pure)

    Abstract

    In this paper we describe our intended approach for the verification of software written in imperative programming languages. We base our approach on model checking of graph transition systems, where each state is a graph and the transitions are 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 allows us to investigate the use of graph abstractions, which can mitigate the combinatorial explosion inherent to model checking. In addition to presenting our planned approach, we reason about its feasibility, and, by providing a brief comparison to other existing methods, we highlight the benefits and drawbacks that are expected.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages12
    Publication statusPublished - Apr 2009

    Publication series

    NameCTIT Technical Report Series
    PublisherCentre for Telematics and Information Technology, University of Twente
    No.TR-CTIT-10-03
    ISSN (Print)1381-3625

    Keywords

    • METIS-265766
    • EWI-17136
    • Software Verification
    • Graph Transformation
    • Graph Abstraction
    • Model Checking
    • Abstract Interpretation
    • IR-69551

    Cite this