Name
Abstract | ||
|---|---|---|
This research started with an algebra for reasoning about rely/guarantee concurrency for a shared memory model. The approach taken led to a more abstract algebra of atomic steps, in which atomic steps synchronise (rather than interleave) when composed in parallel. The algebra of rely/guarantee concurrency then becomes an interpretation of the more abstract algebra. Many of the core properties needed for rely/guarantee reasoning can be shown to hold in the abstract algebra where their proofs are simpler and hence allow a higher degree of automation. Moreover, the realisation that the synchronisation mechanisms of standard process algebras, such as CSP and CCS/SCCS, can be interpreted in our abstract algebra gives evidence of its unifying power. The algebra has been encoded in Isabelle/HOL to provide a basis for tool support. |
Year | DOI | Venue |
|---|---|---|
2016 | 10.1007/978-3-319-48989-6_22 | Lecture Notes in Computer Science |
DocType | Volume | ISSN |
Conference | 9995 | 0302-9743 |
Citations | PageRank | References |
5 | 0.49 | 10 |
Authors | ||
5 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ian J. Hayes | 1 | 634 | 62.03 |
| Robert Colvin | 2 | 68 | 8.67 |
| Larissa Meinicke | 3 | 120 | 8.19 |
| Kirsten Winter | 4 | 46 | 3.24 |
| Andrius Velykis | 5 | 9 | 2.28 |