A sound and complete reasoning system for asynchronous communication with shared futures

DOI10.1016/j.jlamp.2014.03.003zbMath1371.68190OpenAlexW2037688588MaRDI QIDQ465485

Crystal Chang Din, Olaf Owe

Publication date: 23 October 2014

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.2014.03.003

zbMATH Keywords

distributed systemsoperational semanticsHoare logiccompositional reasoningconcurrent objectscommunication history

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) 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 (5)

On detecting over-eager concurrency in asynchronously communicating concurrent object systems ⋮ Global Reproducibility Through Local Control for Distributed Active Objects ⋮ A secrecy-preserving language for distributed and object-oriented systems ⋮ Stateful Behavioral Types for Active Objects ⋮ An evaluation of interaction paradigms for active objects

Uses Software

• Spec#
• Multilisp
• Java Jr

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Observable behavior of distributed systems: component reasoning for concurrent objects
• Lazy behavioral subtyping
• A proof technique for parallel programs
• Behavioral interface description of an object-oriented language with futures and promises
• Defining liveness
• Axiomatic treatment of processes with shared variables revisited
• A system for compositional verification of asynchronous objects
• Formalising Java RMI with explicit code mobility
• Specification and Development of Interactive Systems
• Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects
• Axiomatic semantics of communicating sequential processes
• MULTILISP: a language for concurrent symbolic computation
• Ten Years of Hoare's Logic: A Survey—Part I
• Compositional Reasoning about Shared Futures
• Programming Languages and Systems
• A Complete Guide to the Future
• Programming Languages and Systems
• A Hoare logic for dynamic networks of asynchronously communicating deterministic processes

This page was built for publication: A sound and complete reasoning system for asynchronous communication with shared futures