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 language | Undefined |
---|---|
Title of host publication | Proceedings of the 13th International Conference on Software Engineering and Formal Methods (SEFM 2015) |
Editors | Radu Calinescu, Bernhard Rumpe |
Place of Publication | Switzerland |
Publisher | Springer |
Pages | 84-98 |
Number of pages | 15 |
ISBN (Print) | 978-3-319-22968-3 |
DOIs | |
Publication status | Published - Sept 2015 |
Event | 13th International Conference on Software Engineering and Formal Methods, SEFM 2015 - York, United Kingdom Duration: 7 Sept 2015 → 11 Sept 2015 Conference number: 13 https://www.cs.york.ac.uk/sefm2015/ |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer International Publishing |
Volume | 9276 |
ISSN (Print) | 0302-9743 |
ISSN (Electronic) | 1611-3349 |
Conference
Conference | 13th International Conference on Software Engineering and Formal Methods, SEFM 2015 |
---|---|
Abbreviated title | SEFM |
Country/Territory | United Kingdom |
City | York |
Period | 7/09/15 → 11/09/15 |
Internet address |
Keywords
- EWI-26513
- METIS-315065
- IR-98398