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

    14 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 - Sep 2015
    Event13th International Conference on Software Engineering and Formal Methods, SEFM 2015 - York, United Kingdom
    Duration: 7 Sep 201511 Sep 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
    CountryUnited Kingdom
    CityYork
    Period7/09/1511/09/15
    Internet address

    Keywords

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

    Cite this

    Blom, S., Huisman, M., & Zaharieva, M. (2015). History-Based Verification of Functional Behaviour of Concurrent Programs. In R. Calinescu, & B. Rumpe (Eds.), Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015) (pp. 84-98). (Lecture Notes in Computer Science; Vol. 9276). Switzerland: Springer. https://doi.org/10.1007/978-3-319-22969-0_6