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

11 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
Blom, Stefan ; Huisman, Marieke ; Zaharieva, M. / History-Based Verification of Functional Behaviour of Concurrent Programs. Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015). editor / Radu Calinescu ; Bernhard Rumpe. Switzerland : Springer, 2015. pp. 84-98 (Lecture Notes in Computer Science).
@inproceedings{2aceb8e327794196995c32619aa85ce5,
title = "History-Based Verification of Functional Behaviour of Concurrent Programs",
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.",
keywords = "EWI-26513, METIS-315065, IR-98398",
author = "Stefan Blom and Marieke Huisman and M. Zaharieva",
note = "10.1007/978-3-319-22969-0_6",
year = "2015",
month = "9",
doi = "10.1007/978-3-319-22969-0_6",
language = "Undefined",
isbn = "978-3-319-22968-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "84--98",
editor = "Radu Calinescu and Bernhard Rumpe",
booktitle = "Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015)",

}

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). Lecture Notes in Computer Science, vol. 9276, Springer, Switzerland, pp. 84-98, 13th International Conference on Software Engineering and Formal Methods, SEFM 2015, York, United Kingdom, 7/09/15. https://doi.org/10.1007/978-3-319-22969-0_6

History-Based Verification of Functional Behaviour of Concurrent Programs. / Blom, Stefan; Huisman, Marieke; Zaharieva, M.

Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015). ed. / Radu Calinescu; Bernhard Rumpe. Switzerland : Springer, 2015. p. 84-98 (Lecture Notes in Computer Science; Vol. 9276).

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

TY - GEN

T1 - History-Based Verification of Functional Behaviour of Concurrent Programs

AU - Blom, Stefan

AU - Huisman, Marieke

AU - Zaharieva, M.

N1 - 10.1007/978-3-319-22969-0_6

PY - 2015/9

Y1 - 2015/9

N2 - 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.

AB - 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.

KW - EWI-26513

KW - METIS-315065

KW - IR-98398

U2 - 10.1007/978-3-319-22969-0_6

DO - 10.1007/978-3-319-22969-0_6

M3 - Conference contribution

SN - 978-3-319-22968-3

T3 - Lecture Notes in Computer Science

SP - 84

EP - 98

BT - Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015)

A2 - Calinescu, Radu

A2 - Rumpe, Bernhard

PB - Springer

CY - Switzerland

ER -

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