Experiments with Concurrent Kleene Algebra

Add 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.