Concurrent Kleene algebra and its foundations

DOI10.1016/J.JLAP.2011.04.005zbMath1278.68176OpenAlexW2096490078WikidataQ114851547 ScholiaQ114851547MaRDI QIDQ549679

Ian Wehrman, Bernhard Möller, Georg Struth, C. A. R. Hoare

Publication date: 18 July 2011

Published in: The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL: https://opus.bibliothek.uni-augsburg.de/opus4/frontdoor/index/index/docId/38907

zbMATH Keywords

concurrencydependenceKleene algebraHoare calculusrely/guarantee calculus

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Related Items (46)

Convolution as a Unifying Concept ⋮ Taming Multirelations ⋮ Weighted synchronous automata ⋮ Developments in concurrent Kleene algebra ⋮ Concurrent Kleene algebra with tests and branching automata ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Observation-Based Concurrent Program Logic for Relaxed Memory Consistency Models ⋮ Schedulers and Finishers: On Generating the Behaviours of an Event Structure ⋮ Algebraic coherent confluence and higher globular Kleene algebras ⋮ Generalised rely-guarantee concurrency: an algebraic foundation ⋮ ST-structures ⋮ Convolution and concurrency ⋮ Laws of Programming for References ⋮ Modeling Quantitative Aspects of Concurrent Systems Using Weighted Petri Net Transducers ⋮ Exploring an Interface Model for CKA ⋮ A Program Construction and Verification Tool for Separation Logic ⋮ A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency ⋮ Posets with interfaces as a model for concurrency ⋮ Designing a semantic model for a wide-spectrum language with concurrency ⋮ Generating Posets Beyond N ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Proving language inclusion and equivalence by coinduction ⋮ In praise of algebra ⋮ Catoids and modal convolution algebras ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ \( \ell r\)-multisemigroups, modal quantales and the origin of locality ⋮ Abstract strategies and coherence ⋮ On algebra of program correctness and incorrectness ⋮ On tools for completeness of Kleene algebra with hypotheses ⋮ A Discrete Geometric Model of Concurrent Program Execution ⋮ Reordering Derivatives of Trace Closures of Regular Languages. ⋮ Probabilistic rely-guarantee calculus ⋮ Completely and partially executable sequences of actions in deontic context ⋮ On the algebraic structure of Weihrauch degrees ⋮ On Weighted Petri Net Transducers ⋮ Mitigating covert channels based on analysis of the potential for communication ⋮ Unifying Semantics for Concurrent Programming ⋮ Concurrent Kleene algebra and its foundations ⋮ Unnamed Item ⋮ Schedulers and finishers: on generating and filtering the behaviours of an event structure ⋮ Unnamed Item ⋮ Generic Models of the Laws of Programming ⋮ Unnamed Item ⋮ Modal algebra and Petri nets ⋮ A semantics and a logic for \textit{Fuzzy Arden Syntax} ⋮ On the relation between concurrent separation logic and concurrent Kleene algebra

Uses Software

• Prover9
• Mace4

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Concurrent Kleene algebra and its foundations
• Fixed-point calculus
• Synchronous Kleene algebra
• Resources, concurrency, and local reasoning
• Graphical models of separation logic
• Modeling concurrency with partial orders
• The equational theory of pomsets
• A calculus of communicating systems
• A completeness theorem for Kleene algebras and the algebra of regular events
• Concurrent Kleene Algebra
• Foundations of Concurrent Kleene Algebra
• Semiring-based constraint satisfaction and optimization
• From μCRL to mCRL2
• Kleene algebra with domain
• An axiomatic basis for computer programming

This page was built for publication: Concurrent Kleene algebra and its foundations