History-Based Verification of Functional Behaviour of Concurrent Programs

Stefan Blom, Marieke Huisman, M. Zaharieva

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 International Publishing
Pages84-98
Number of pages15
ISBN (Print)978-3-319-22968-3
DOIs
StatePublished - Sep 2015
Event13th International Conference on Software Engineering and Formal Methods, SEFM 2015 - York, United Kingdom

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

Fingerprint

History

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 International Publishing. DOI: 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). ed. / Radu Calinescu; Bernhard Rumpe. Switzerland : Springer International Publishing, 2015. p. 84-98 (Lecture Notes in Computer Science; Vol. 9276).

Research output: Scientific - peer-reviewConference contribution

@inbook{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",
isbn = "978-3-319-22968-3",
series = "Lecture Notes in Computer Science",
publisher = "Springer International Publishing",
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 International Publishing, Switzerland, pp. 84-98, 13th International Conference on Software Engineering and Formal Methods, SEFM 2015, York, United Kingdom, 7-11 September. DOI: 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 International Publishing, 2015. p. 84-98 (Lecture Notes in Computer Science; Vol. 9276).

Research output: Scientific - peer-reviewConference contribution

TY - CHAP

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)

PB - Springer International Publishing

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 International Publishing. 2015. p. 84-98. (Lecture Notes in Computer Science). Available from, DOI: 10.1007/978-3-319-22969-0_6