Loading...
Please wait, while we are loading the content...
Similar Documents
Verifying Functional Behaviour of Concurrent Programs
| Content Provider | ACM Digital Library |
|---|---|
| Author | Blom, Stefan Zaharieva-Stojanovski, Marina Huisman, Marieke |
| 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. |
| Starting Page | 1 |
| Ending Page | 6 |
| Page Count | 6 |
| File Format | |
| ISBN | 9781450328661 |
| DOI | 10.1145/2635631.2635849 |
| Language | English |
| Publisher | Association for Computing Machinery (ACM) |
| Publisher Date | 2014-07-28 |
| Publisher Place | New York |
| Access Restriction | Subscribed |
| Subject Keyword | Modular verification Separation logic Concurrency Histories |
| Content Type | Text |
| Resource Type | Article |
