scientific article; zbMATH DE number 194539

Publication date: 5 June 1993

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

communication systolic arrays fault tolerance efficient parallel algorithms mutual exclusion UNITY termination detection garbage collection dining philosophers stability detection

Mathematics Subject Classification ID

Introductory exposition (textbooks, tutorial papers, etc.) pertaining to computer science (68-01) Distributed algorithms (68W15)

Related Items (only showing first 100 items - show all)

Conditional rewriting logic: Deduction, models and concurrency ⋮ A case study in the mechanical verification of fault tolerance ⋮ Composite registers ⋮ Distributed maximum maintenance on hierarchically divided graphs ⋮ A case study in transformational design of concurrent systems ⋮ Constraining interference in an object-based design method ⋮ Application of the composition principle to unity-like specifications ⋮ Property preserving abstractions under parallel composition ⋮ Generic systolic arrays: A methodology for systolic design ⋮ A verification framework for agent programming with declarative goals ⋮ Temporal Logic and Fair Discrete Systems ⋮ Combining Model Checking and Deduction ⋮ On the correctness of a distributed memory Gröbner basis algorithm ⋮ Invariants, composition, and substitution ⋮ Deriving Real-Time Action Systems Controllers from Multiscale System Specifications ⋮ A Normalized Form for FIFO Protocols Traces, Application to the Replay of Mode-based Protocols ⋮ A new explanation of the glitch phenomenon ⋮ Bounded delay for a free address ⋮ DUALITY: A simple formalism for the analysis of UNITY ⋮ Applying abstraction and formal specification in numerical software design ⋮ Specification and refinement of networks of asynchronously communicating agents using the assumption/commitment paradigm ⋮ Superposition refinement of reactive systems ⋮ Program composition via unification ⋮ Generic Proof Scores for Generate & Check Method in CafeOBJ ⋮ Logical foundations for compositional verification and development of concurrent programs in UNITY ⋮ On mechanizing proofs within a complete proof system for Unity ⋮ Tournaments for mutual exclusion: verification and concurrent complexity ⋮ rCOS: Defining Meanings of Component-Based Software Architectures ⋮ Simulation relations for fault-tolerance ⋮ Rewriting logic as a semantic framework for concurrency: a progress report ⋮ A framework for automated distributed implementation of component-based models ⋮ The asynchronous committee meeting problem ⋮ Using refinement calculus techniques to prove linearizability ⋮ Security invariants in discrete transition systems ⋮ Computing with multiple discrete flows ⋮ Concurrent maintenance of rings ⋮ Compositional Verification for Component-Based Systems and Application ⋮ Adaptive solutions to the mutual exclusion problem ⋮ Naming symmetric processes using shared variables ⋮ Wait-free linearization with an assertional proof ⋮ Wait-free linearization with a mechanical proof ⋮ A fast, scalable mutual exclusion algorithm ⋮ Knowledge-based programs ⋮ Using local-spin k -exclusion algorithms to improve wait-free object implementations ⋮ Automatic verification for a class of distributed systems ⋮ A note on knowledge-based programs and specifications ⋮ Asynchronous group mutual exclusion ⋮ Hundreds of impossibility results for distributed computing ⋮ Action systems in incremental and aspect-oriented modeling ⋮ Safety assurance via on-line monitoring ⋮ Unnamed Item ⋮ On Reasoning About Rings ⋮ Decidability of a partial order based temporal logic ⋮ Reasoning about programs by exploiting the environment ⋮ Distributed consensus, revisited ⋮ Formalism and method ⋮ Towards a Combination of CafeOBJ and PAT ⋮ Partially Ordered Knowledge Sharing and Fractionated Systems in the Context of other Models for Distributed Computing ⋮ Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs ⋮ An Algebraic Approach to Refinement with Fair Choice ⋮ Abstraction of hardware construction ⋮ A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting ⋮ Streamlining progress-based derivations of concurrent programs ⋮ Unnamed Item ⋮ Algebra Transformation Systems as a Unifying Framework ⋮ Automatic Verification of Bossa Scheduler Properties ⋮ Ensuring completeness of symbolic verification methods for infinite-state systems ⋮ Abstract state machines: a unifying view of models of computation and of system design frameworks ⋮ Linearization in parallel pCRL ⋮ UNITY and Büchi automata ⋮ Partial correctness for probabilistic demonic programs ⋮ A pragmatic behavior subtyping relation based on both states and actions ⋮ Refinement verification of the lazy caching algorithm ⋮ Web Cube ⋮ Interfaces between languages for communicating systems ⋮ Packet efficient implementation of the Omega failure detector ⋮ Specification and analysis of a composition of protocols ⋮ The sliding-window protocol revisited ⋮ Mirror, mirror in my hand: a duality between specifications and models of process behaviour ⋮ State Space Reduction of Linear Processes Using Control Flow Reconstruction ⋮ A simple proof of a simple consensus algorithm ⋮ Process of petri nets extension ⋮ Slicing techniques for verification re-use ⋮ Generate & Check Method for Verifying Transition Systems in CafeOBJ ⋮ Coordinating action systems ⋮ Factorizing fault tolerance. ⋮ Quantitative program logic and expected time bounds in probabilistic distributed algorithms. ⋮ Specification and verification of concurrent programs through refinements ⋮ A walk over the shortest path: Dijkstra's algorithm viewed as fixed-point computation. ⋮ The shortest path in parallel ⋮ Event-based proof of the mutual exclusion property of Peterson's algorithm ⋮ Program composition via unification ⋮ Mechanizing a process algebra for network protocols ⋮ Correct translation of data parallel assignment onto array processors ⋮ Error in the UNITY substitution rule for subscripted operators ⋮ Progress properties for empty \textsc{Unity} programs ⋮ Properties of concurrent programs ⋮ Property preserving abstractions for the verification of concurrent systems ⋮ Focus points and convergent process operators: A proof strategy for protocol verification ⋮ Verifying a distributed list system: A case history

This page was built for publication: