A discrete geometric model of concurrent program execution

DOI10.1007/978-3-319-52228-9_1MaRDI QIDQ2971172zbMATH OpenOpenAlexFDO

Authors Bernhard Möller, Martin Müller, Georg Struth, Tony 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

concurrent Kleene algebralaws of programmingrefinementsemantic modelstrace algebraunifying theories

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Concurrent Kleene Algebra
• Geometry and concurrency: a user's guide
• Concurrent Kleene algebra and its foundations
• Formal relationships between geometrical and classical models for concurrency
• The geometry of semaphore programs

Cites work

• A formal hierarchy of weak memory models
• A program construction and verification tool for separation logic
• A semantics for concurrent separation logic
• Building program construction and verification tools from algebraic principles
• Concurrent Kleene algebra and its foundations
• Developments in concurrent Kleene algebra
• scientific article; zbMATH DE number 3366846 (Why is no real title available?)
• Isabelle/HOL. A proof assistant for higher-order logic
• LSCs: Breathing life into message sequence charts
• On locality and the exchange law for concurrent processes
• On powerdomains and modality
• On the relation between concurrent separation logic and concurrent Kleene algebra
• Power structures
• The validity of equations of complex algebras
• Unifying theories for logic programming
• Varieties of complex algebras

Cited in

(6)

• A ``geometric view of the dynamics of trajectories of computer programs
• The geometry of semaphore programs
• Geometry and concurrency: a user's guide
• Generating Posets Beyond N
• Simplicial Models for Concurrency
• Jifeng He at Oxford and beyond: an appreciation

Describes a project that uses

Uses Software

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

This page was built for publication: A discrete geometric model of concurrent program execution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2971172)