Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects
From MaRDI portal
Publication:2864507
DOI10.1016/j.entcs.2008.04.084zbMath1277.68056OpenAlexW2159887230MaRDI QIDQ2864507
Johan Dovland, Olaf Owe, Einar Broch Johnsen
Publication date: 6 December 2013
Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.entcs.2008.04.084
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
A system for compositional verification of asynchronous objects ⋮ Observable behavior of distributed systems: component reasoning for concurrent objects ⋮ A sound and complete reasoning system for asynchronous communication with shared futures ⋮ Incremental reasoning with lazy behavioral subtyping for multiple inheritance ⋮ Lazy behavioral subtyping ⋮ An operational semantics for object-oriented concepts based on the class hierarchy ⋮ Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A proof technique for parallel programs
- Ten years of Hoare's logic: A survey. II: Nondeterminism
- Defining liveness
- An assertion-based proof system for multithreaded Java
- From object-orientation to formal methods. Essays in memory of Ole-Johan Dahl.
- Specification and Development of Interactive Systems
- Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects
- Axiomatic semantics of communicating sequential processes
- Ten Years of Hoare's Logic: A Survey—Part I
- Guarded commands, nondeterminacy and formal derivation of programs
- Formal Methods for Components and Objects
- A Hoare logic for dynamic networks of asynchronously communicating deterministic processes