Compositional reasoning about active objects with shared futures

DOI10.1007/s00165-014-0322-yzbMath1343.68166OpenAlexW2089178595MaRDI QIDQ890481

Olaf Owe, Crystal Chang Din

Publication date: 10 November 2015

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-014-0322-y

zbMATH Keywords

distributed systemsoperational semanticsdynamic logicobject orientationasynchronous communicationcompositional reasoningconcurrent objectscommunication historyshared futures

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) 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

A lightweight approach to smart contracts supporting safety, security, and privacy ⋮ KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS ⋮ Modeling Actor Systems Using Dynamic I/O Automata ⋮ The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics

Uses Software

• MapReduce
• Eiffel
• Maude
• Multilisp
• Java Jr

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Observable behavior of distributed systems: component reasoning for concurrent objects
• A proof technique for parallel programs
• Behavioral interface description of an object-oriented language with futures and promises
• Cameo: an alternative model of concurrency for Eiffel
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Defining liveness
• Conditional rewriting logic as a unified model of concurrency
• A system for compositional verification of asynchronous objects
• Formalising Java RMI with explicit code mobility
• Specification and Development of Interactive Systems
• Axiomatic semantics of communicating sequential processes
• MULTILISP: a language for concurrent symbolic computation
• Compositional Reasoning about Shared Futures
• Programming Languages and Systems
• Object-Oriented Specification and Open Distributed Systems
• KeY: A Formal Method for Object-Oriented Systems
• A Complete Guide to the Future
• A Hoare logic for dynamic networks of asynchronously communicating deterministic processes