Verifying Functional Behaviour of Concurrent Programs

M. Zaharieva, Marieke Huisman, Stefan Blom

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

1 Citation (Scopus)
46 Downloads (Pure)

Abstract

Specifying the functional behaviour of a concurrent program can often be quite troublesome: it is hard to provide a stable method contract that can not be invalidated by other threads. In this paper we propose a novel modular technique for specifying and verifying behavioural properties in concurrent programs. Our approach uses history-based specifications. A history is a process algebra term built of actions, where each action represents an update over a heap location. Instead of describing the object's precise state, a method contract may describe the method's behaviour in terms of actions recorded in the history. The client class can later use the history to reason about the concrete state of the object. Our approach allows providing simple and intuitive specifications, while the logic is a simple extension of permission-based separation logic.
Original languageUndefined
Title of host publicationFTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs
EditorsD. Pearce
Place of PublicationNew York
PublisherAssociation for Computing Machinery (ACM)
Pages4:1-4:6
Number of pages6
ISBN (Print)978-1-4503-2866-1
DOIs
Publication statusPublished - Jul 2014
Event16th Workshop on Formal Techniques for Java-like Programs, FTfJP 2014 - Uppsala, Sweden
Duration: 28 Jul 201428 Jul 2014
Conference number: 16
http://ecs.victoria.ac.nz/Events/FTfJP2014/

Publication series

Name
PublisherACM

Workshop

Workshop16th Workshop on Formal Techniques for Java-like Programs, FTfJP 2014
Abbreviated titleFTfJP
CountrySweden
CityUppsala
Period28/07/1428/07/14
Internet address

Keywords

  • EWI-24914
  • CR-D.1.3
  • CR-D.2.4
  • concurrent programsmodular verificationbehavioural specifications
  • METIS-305947
  • Modular Verification
  • IR-91896
  • Concurrent programs
  • behavioural specifications

Cite this

Zaharieva, M., Huisman, M., & Blom, S. (2014). Verifying Functional Behaviour of Concurrent Programs. In D. Pearce (Ed.), FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs (pp. 4:1-4:6). New York: Association for Computing Machinery (ACM). https://doi.org/10.1145/2635631.2635849
Zaharieva, M. ; Huisman, Marieke ; Blom, Stefan. / Verifying Functional Behaviour of Concurrent Programs. FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs. editor / D. Pearce. New York : Association for Computing Machinery (ACM), 2014. pp. 4:1-4:6
@inproceedings{c0081c376f294fa6956cb069c672f5f8,
title = "Verifying Functional Behaviour of Concurrent Programs",
abstract = "Specifying the functional behaviour of a concurrent program can often be quite troublesome: it is hard to provide a stable method contract that can not be invalidated by other threads. In this paper we propose a novel modular technique for specifying and verifying behavioural properties in concurrent programs. Our approach uses history-based specifications. A history is a process algebra term built of actions, where each action represents an update over a heap location. Instead of describing the object's precise state, a method contract may describe the method's behaviour in terms of actions recorded in the history. The client class can later use the history to reason about the concrete state of the object. Our approach allows providing simple and intuitive specifications, while the logic is a simple extension of permission-based separation logic.",
keywords = "EWI-24914, CR-D.1.3, CR-D.2.4, concurrent programsmodular verificationbehavioural specifications, METIS-305947, Modular Verification, IR-91896, Concurrent programs, behavioural specifications",
author = "M. Zaharieva and Marieke Huisman and Stefan Blom",
note = "10.1145/2635631.2635849",
year = "2014",
month = "7",
doi = "10.1145/2635631.2635849",
language = "Undefined",
isbn = "978-1-4503-2866-1",
publisher = "Association for Computing Machinery (ACM)",
pages = "4:1--4:6",
editor = "D. Pearce",
booktitle = "FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs",
address = "United States",

}

Zaharieva, M, Huisman, M & Blom, S 2014, Verifying Functional Behaviour of Concurrent Programs. in D Pearce (ed.), FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs. Association for Computing Machinery (ACM), New York, pp. 4:1-4:6, 16th Workshop on Formal Techniques for Java-like Programs, FTfJP 2014, Uppsala, Sweden, 28/07/14. https://doi.org/10.1145/2635631.2635849

Verifying Functional Behaviour of Concurrent Programs. / Zaharieva, M.; Huisman, Marieke; Blom, Stefan.

FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs. ed. / D. Pearce. New York : Association for Computing Machinery (ACM), 2014. p. 4:1-4:6.

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

TY - GEN

T1 - Verifying Functional Behaviour of Concurrent Programs

AU - Zaharieva, M.

AU - Huisman, Marieke

AU - Blom, Stefan

N1 - 10.1145/2635631.2635849

PY - 2014/7

Y1 - 2014/7

N2 - Specifying the functional behaviour of a concurrent program can often be quite troublesome: it is hard to provide a stable method contract that can not be invalidated by other threads. In this paper we propose a novel modular technique for specifying and verifying behavioural properties in concurrent programs. Our approach uses history-based specifications. A history is a process algebra term built of actions, where each action represents an update over a heap location. Instead of describing the object's precise state, a method contract may describe the method's behaviour in terms of actions recorded in the history. The client class can later use the history to reason about the concrete state of the object. Our approach allows providing simple and intuitive specifications, while the logic is a simple extension of permission-based separation logic.

AB - Specifying the functional behaviour of a concurrent program can often be quite troublesome: it is hard to provide a stable method contract that can not be invalidated by other threads. In this paper we propose a novel modular technique for specifying and verifying behavioural properties in concurrent programs. Our approach uses history-based specifications. A history is a process algebra term built of actions, where each action represents an update over a heap location. Instead of describing the object's precise state, a method contract may describe the method's behaviour in terms of actions recorded in the history. The client class can later use the history to reason about the concrete state of the object. Our approach allows providing simple and intuitive specifications, while the logic is a simple extension of permission-based separation logic.

KW - EWI-24914

KW - CR-D.1.3

KW - CR-D.2.4

KW - concurrent programsmodular verificationbehavioural specifications

KW - METIS-305947

KW - Modular Verification

KW - IR-91896

KW - Concurrent programs

KW - behavioural specifications

U2 - 10.1145/2635631.2635849

DO - 10.1145/2635631.2635849

M3 - Conference contribution

SN - 978-1-4503-2866-1

SP - 4:1-4:6

BT - FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs

A2 - Pearce, D.

PB - Association for Computing Machinery (ACM)

CY - New York

ER -

Zaharieva M, Huisman M, Blom S. Verifying Functional Behaviour of Concurrent Programs. In Pearce D, editor, FTfJP'14: Proceedings of 16th Workshop on Formal Techniques for Java-like Programs. New York: Association for Computing Machinery (ACM). 2014. p. 4:1-4:6 https://doi.org/10.1145/2635631.2635849