| | |
| | |
Stat |
Members: 3667 Articles: 2'599'751 Articles rated: 2609
09 February 2025 |
|
| | | |
|
Article overview
| |
|
An algebra of synchronous atomic steps | Ian J. Hayes
; Robert Colvin
; Larissa Meinicke
; Kirsten Winter
; Andrius Velykis
; | Date: |
1 Sep 2016 | 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. | Source: | arXiv, 1609.0118 | Services: | Forum | Review | PDF | Favorites |
|
|
No review found.
Did you like this article?
Note: answers to reviews or questions about the article must be posted in the forum section.
Authors are not allowed to review their own article. They can use the forum section.
|
| |
|
|
|