History-Based Verification of Functional Behaviour of Concurrent Programs

Stefan Blom, Marieke Huisman, M. Zaharieva

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

    47 Downloads (Pure)

    Abstract

    We extend permission-based separation logic with a history-based mechanism to simplify the verification of functional properties in concurrent programs. This allows one to specify the local behaviour of a method intuitively in terms of actions added to a local history; local histories can be combined into global histories, and by resolving the global histories, the reachable state properties can be determined.
    Original languageUndefined
    Title of host publicationProceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015)
    EditorsRadu Calinescu, Bernhard Rumpe
    Place of PublicationSwitzerland
    PublisherSpringer
    Pages84-98
    Number of pages15
    ISBN (Print)978-3-319-22968-3
    DOIs
    Publication statusPublished - Sept 2015
    Event13th International Conference on Software Engineering and Formal Methods, SEFM 2015 - York, United Kingdom
    Duration: 7 Sept 201511 Sept 2015
    Conference number: 13
    https://www.cs.york.ac.uk/sefm2015/

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer International Publishing
    Volume9276
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349

    Conference

    Conference13th International Conference on Software Engineering and Formal Methods, SEFM 2015
    Abbreviated titleSEFM
    Country/TerritoryUnited Kingdom
    CityYork
    Period7/09/1511/09/15
    Internet address

    Keywords

    • EWI-26513
    • METIS-315065
    • IR-98398

    Cite this