Abstract
A concurrent Kleene algebra offers, next to choice and iteration, operators for sequential and concurrent composition, related by an inequational form of the exchange law. We show applicability of the algebra to a partially-ordered trace model of program execution semantics and demonstrate its usefulness by validating familiar proof rules for sequential programs (Hoare triples) and for concurrent ones (Jones's rely/guarantee calculus). This involves an algebraic notion of invariants; for these the exchange inequation strengthens to an equational distributivity law. Most of our reasoning has been checked by computer. © 2009 Springer Berlin Heidelberg.
Cite
CITATION STYLE
Hoare, C. A. R. T., Möller, B., Struth, G., & Wehrman, I. (2009). Concurrent kleene algebra. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5710 LNCS, pp. 399–414). https://doi.org/10.1007/978-3-642-04081-8_27
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
