Developments in concurrent Kleene algebra
From MaRDI portal
Publication:299202
DOI10.1016/j.jlamp.2015.09.012zbMath1344.68149OpenAlexW2206274334WikidataQ114851593 ScholiaQ114851593MaRDI QIDQ299202
Bernhard Möller, Georg Struth, Stephan van Staden, Huibiao Zhu, C. A. R. Hoare
Publication date: 22 June 2016
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlamp.2015.09.012
Algebraic theory of languages and automata (68Q70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
A UTP approach for rTiMo, Unnamed Item, Contextuality in distributed systems, A Discrete Geometric Model of Concurrent Program Execution, A process calculus BigrTiMo of mobile systems and its formal semantics, Unnamed Item
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Programming and automating mathematics in the Tarski-Kleene hierarchy
- Algebraic separation logic
- Concurrent Kleene algebra and its foundations
- Internal axioms for domain semirings
- Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language
- Free shuffle algebras in language varieties
- Relation algebras
- Denotational semantics and its algebraic derivation for an event-driven system-level language
- Graphical models of separation logic
- On powerdomains and modality
- Systolic algorithms as programs
- The equational theory of pomsets
- A calculus of communicating systems
- On the completeness of the inductive assertion method
- A completeness theorem for Kleene algebras and the algebra of regular events
- Isabelle/HOL. A proof assistant for higher-order logic
- Power structures
- A language of specified programs
- Modal algebra and Petri nets
- Varieties of complex algebras
- Relational Knowledge Discovery
- Transitive Separation Logic
- Automated Reasoning in Higher-Order Regular Algebra
- Exploring an Interface Model for CKA
- A Program Construction and Verification Tool for Separation Logic
- The validity of equations of complex algebras
- Infinitary varieties of structures closed under the formation of complex structures
- Mechanical Approach to Linking Operational Semantics and Algebraic Semantics for Verilog Using Maude
- Formal Derivation of Concurrent Garbage Collectors
- Quantales and Temporal Logics
- Modalities, Relations, and Learning
- Process algebra for synchronous communication
- A Theory of Communicating Sequential Processes
- Laws of programming
- Guarded commands, nondeterminacy and formal derivation of programs
- The Logic of Bunched Implications
- Refinement Calculus
- The specification statement
- Proving that non-blocking algorithms don't block
- Kleene algebra with domain
- Concurrent Kleene Algebra with Tests
- Algebras for Program Correctness in Isabelle/HOL
- Completeness Theorems for Bi-Kleene Algebras and Series-Parallel Rational Pomset Languages
- A Structural Proof of the Soundness of Rely/guarantee Rules
- Two Complete Axiom Systems for the Algebra of Regular Events
- An axiomatic basis for computer programming
