A Discrete Geometric Model of Concurrent Program Execution

DOI10.1007/978-3-319-52228-9_1zbMath1483.68086OpenAlexW2570187344MaRDI QIDQ2971172

Georg Struth, Bernhard Möller, Martin Eric Müller, C. A. R. Hoare

Publication date: 4 April 2017

Published in: Unifying Theories of Programming (Search for Journal in Brave)

Full work available at URL: http://eprints.whiterose.ac.uk/116278/1/UTP16-New6.pdf

zbMATH Keywords

refinementsemantic modelsconcurrent Kleene algebralaws of programmingtrace algebraunifying theories

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) 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 (2)

Generating Posets Beyond N ⋮ Jifeng He at Oxford and beyond: an appreciation

Uses Software

• Isabelle
• Isabelle/HOL
• Archive Formal Proofs
• Algebraic_VCs

Cites Work

• Unnamed Item
• Unnamed Item
• Developments in concurrent Kleene algebra
• Concurrent Kleene algebra and its foundations
• Building program construction and verification tools from algebraic principles
• A semantics for concurrent separation logic
• On powerdomains and modality
• Isabelle/HOL. A proof assistant for higher-order logic
• Power structures
• On the relation between concurrent separation logic and concurrent Kleene algebra
• A formal hierarchy of weak memory models
• Varieties of complex algebras
• A Program Construction and Verification Tool for Separation Logic
• On Locality and the Exchange Law for Concurrent Processes
• The validity of equations of complex algebras
• LSCs: Breathing life into message sequence charts

This page was built for publication: A Discrete Geometric Model of Concurrent Program Execution