Silva, A; (2019) An algebraic framework to reason about concurrency. In: Chattopadhyay, A and Gastin, P, (eds.) Proceedings of the 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019). (pp. 6.1). Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik: Dagstuhl, Germany.

Preview

Text LIPIcs-FSTTCS-2019-6.pdf - Published Version Download (209kB) | Preview

Abstract

Kleene algebra with tests (KAT) is an algebraic framework for reasoning about the control flow of sequential programs. Hoare, Struth, and collaborators proposed a concurrent extension of Kleene Algebra (CKA) as a first step towards developing algebraic reasoning for concurrent programs. Completing their research program and extending KAT to encompass concurrent behaviour has however proven to be more challenging than initially expected. The core problem appears because when generalising KAT to reason about concurrent programs, axioms native to KAT in conjunction with expected axioms for reasoning about concurrency lead to an unexpected equation about programs. In this talk, we will revise the literature on CKA(T) and explain the challenges and solutions in the development of an algebraic framework for concurrency. The talk is based on a series of papers joint with Tobias Kappé, Paul Brunet, Bas Luttik, Jurriaan Rot, Jana Wagemaker, and Fabio Zanasi [Tobias Kappé et al., 2017; Tobias Kappé et al., 2019; Kappé et al., 2018]. Additional references can be found on the CoNeCo project website: https://coneco-project.org/.

Download activity - last month

Export as XMLJSONCSV

Download activity - last 12 months

Export as CSVJSONXML

Downloads by country - last 12 months

Export as JSONCSVXML

Archive Staff Only

View Item