COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Isaac Newton Institute Seminar Series > Experiments with Concurrent Kleene Algebra

## Experiments with Concurrent Kleene AlgebraAdd to your list(s) Download to your calendar using vCal - Bernhard MÃ¶ller (UniversitÃ¤t Augsburg)
- Tuesday 05 July 2022, 09:30-10:30
- Seminar Room 1, Newton Institute.
If you have a question about this talk, please contact nobody. VS2W01 - Vistas in Verified Software This talk is on the foundational side. In 2009, Concurrent Kleene Algebra (briefly CKA ) was defined as an extension of Kleene Algebra, adding to sequential composition several variants of concurrent composition while preserving the standard laws. The aim was to allow, in parallel to operational or assertion-logical deduction, also algebraic, (in)equational proofs about concurrent systems. This is particularly interesting, since (in)equational reasoning is very suitable for semi-automatic or even automatic proofs. CKA has met considerable interest. We discuss some new twists about it. - We present a new definition technique for partial operators, namely an assume/claim style akin to the rely/guarantee format of program specification. This admits a general way of defining a refinement relation as well as Top and Bottom elements of the refinement order. - We experiment with the graph model of the algebra, in particular how state-like entities could be defined, along with image and inverse image operators. This allows a form of Hoare triples and relates to O’Hearn’s resource view of these. It remains to be seen whether a purely algebraic abstraction of the approach can be found. The talk is based on unpublished joint work with Tony Hoare. This talk is part of the Isaac Newton Institute Seminar Series series. ## This talk is included in these lists:- All CMS events
- Featured lists
- INI info aggregator
- Isaac Newton Institute Seminar Series
- School of Physical Sciences
- Seminar Room 1, Newton Institute
- bld31
Note that ex-directory lists are not shown. |
## Other listsTrust and Cloud Computing Computer Laboratory Systems Research Group Seminar Data mining## Other talksThe technology and commercialisation journey of Evonetix TBA Intraneural neuroprostheses to understand and restore sensory, motor, and autonomic neural functions Industrial Panel (MathWorks, Microsoft, Nvidia) Gateway Science & Engineering |