History-based Verification of Functional Behaviour of Concurrent Programs

Stefan Blom, Marieke Huisman, M. Zaharieva

    Research output: Book/ReportReportProfessional

    7 Citations (Scopus)
    106 Downloads (Pure)

    Abstract

    Modular verification of the functional behaviour of a concurrent program remains a challenge. We propose a new way to achieve this, using histories, modelled as process algebra terms, to keep track of local changes. When threads terminate or synchronise in some other way, local histories are combined into global histories, and by resolving the global histories, the reachable state properties can be determined. Our logic is an extension of permission-based separation logic, which supports expressive and intuitive specifications. We discuss soundness of the approach, and illustrate it on several examples.
    Original languageUndefined
    Place of PublicationEnschede
    PublisherCentre for Telematics and Information Technology (CTIT)
    Number of pages25
    Publication statusPublished - 9 Mar 2015

    Publication series

    NameCTIT Technical Report Series
    PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
    No.TR-CTIT-15-02
    ISSN (Print)1381-3625

    Keywords

    • METIS-312523
    • EWI-25866
    • concurrent programsmodular verificationbehavioural specifications
    • behavioural specifications
    • IR-95383
    • Concurrent programs
    • Modular Verification

    Cite this

    Blom, S., Huisman, M., & Zaharieva, M. (2015). History-based Verification of Functional Behaviour of Concurrent Programs. (CTIT Technical Report Series; No. TR-CTIT-15-02). Enschede: Centre for Telematics and Information Technology (CTIT).