Name
Abstract | ||
|---|---|---|
Linearizability is a key correctness criterion for concurrent software. In our previous work, we have introduced local proof obligations, which, by showing a refinement between an abstract specification and its implementation, imply linearizability of the implementation. The refinement is shown via a process local simulation. We have incorporated the approach of verifying linearizability based on refinement in two rather different proof systems: a predicate logic based approach performing a simulation for two processes and second, an approach based on temporal logic that shows a refinement for an individual process using rely–guarantee reasoning and symbolic execution. To compare both proof techniques, we use an implementation of a multiset as running example. Moreover, we show how ownership annotations have helped us to reduce the proof effort. All proofs are mechanized in the theorem prover KIV. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1016/j.scico.2014.04.001 | Science of Computer Programming |
Keywords | Field | DocType |
Linearizability,Concurrent data types,Interactive verification | Programming language,Computer science,Multiset,Automated theorem proving,Correctness,Theoretical computer science,Mathematical proof,Temporal logic,Proof complexity,Predicate logic,Proof assistant | Journal |
Volume | Issue | ISSN |
96 | P3 | 0167-6423 |
Citations | PageRank | References |
1 | 0.35 | 24 |
Authors | ||
4 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Bogdan Tofan | 1 | 86 | 4.93 |
| Oleg Travkin | 2 | 52 | 5.66 |
| Gerhard Schellhorn | 3 | 769 | 56.43 |
| Heike Wehrheim | 4 | 1013 | 104.85 |