scientific article

zbMath0587.68018MaRDI QIDQ3713577

Jifeng He, Jeff W. Sanders, C. A. R. Hoare

Publication date: 1986

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

implementationnondeterminismdata refinementweakest specificationabstract specificationcorrectness of refinementsimulation of communicating systems

Mathematics Subject Classification ID

Data structures (68P05) Theory of operating systems (68N25)

Related Items (37)

Relational separation logic ⋮ Incompleteness of relational simulations in the blocking paradigm ⋮ Observational purity and encapsulation ⋮ A criterion for atomicity revisited ⋮ Decidability and complexity for quiescent consistency and its variations ⋮ A Sound and Complete Proof Technique for Linearizability of Concurrent Data Structures ⋮ Abstraction for concurrent objects ⋮ The representational entity in physical computing ⋮ Jifeng He at Oxford and beyond: an appreciation ⋮ A pragmatic approach to stateful partial order reduction ⋮ Proving opacity of transactional memory with early release ⋮ On hierarchically developing reactive systems ⋮ Starvation-free mutual exclusion with semaphores ⋮ Relational Concurrent Refinement: Automata ⋮ Of wlp and CSP ⋮ Guarded Operations, Refinement and Simulation ⋮ Bridging arrays and ADTs in recursive proofs ⋮ Simulation Refinement for Concurrency Verification ⋮ More Relational Concurrent Refinement: Traces and Partial Relations ⋮ A single complete rule for data refinement ⋮ Universal extensions to simulate specifications ⋮ Simulation refinement for concurrency verification ⋮ Splitting forward simulations to cope with liveness ⋮ ASM refinement and generalizations of forward simulation in data refinement: a comparison ⋮ Prespecification in data refinement ⋮ Refinement verification of the lazy caching algorithm ⋮ An operational semantics for object-oriented concepts based on the class hierarchy ⋮ On integrating confidentiality and functionality in a formal method ⋮ Introducing extra operations in refinement ⋮ Relational concurrent refinement. III: Traces, partial relations and automata ⋮ A queue based mutual exclusion algorithm ⋮ Verification of compliance for multilevel models in individual trace semantics ⋮ Set-Theoretic Models of Computations ⋮ Objects and classes in Algol-like languages ⋮ Understanding, Explaining, and Deriving Refinement ⋮ Sound and Relaxed Behavioural Inheritance ⋮ Normal form approach to compiler design

This page was built for publication: