UNITY
From MaRDI portal
Software:25375
No author found.
Related Items (only showing first 100 items - show all)
Conditional rewriting logic: Deduction, models and concurrency ⋮ 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 ⋮ Unnamed Item ⋮ Invariants, composition, and substitution ⋮ Constructive Polychronous Systems ⋮ 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 ⋮ Tournaments for mutual exclusion: verification and concurrent complexity ⋮ rCOS: Defining Meanings of Component-Based Software Architectures ⋮ Simulation relations for fault-tolerance ⋮ A framework for automated distributed implementation of component-based models ⋮ Using refinement calculus techniques to prove linearizability ⋮ Security invariants in discrete transition systems ⋮ Computing with multiple discrete flows ⋮ Preserving stabilization while \textit{practically} bounding state space using incorruptible partially synchronized clocks ⋮ 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 ⋮ Automatic verification for a class of distributed systems ⋮ A note on knowledge-based programs and specifications ⋮ Asynchronous group mutual exclusion ⋮ Safety assurance via on-line monitoring ⋮ Unnamed Item ⋮ Formal Reasoning About Causality Analysis ⋮ Decidability of a partial order based temporal logic ⋮ Reasoning about programs by exploiting the environment ⋮ Distributed consensus, revisited ⋮ Knowledge-Based Synthesis of Distributed Systems Using Event Structures ⋮ Formalism and method ⋮ Towards a Combination of CafeOBJ and PAT ⋮ Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs ⋮ An Algebraic Approach to Refinement with Fair Choice ⋮ A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting ⋮ Streamlining progress-based derivations of concurrent programs ⋮ Unnamed Item ⋮ Mechanizing UNITY in Isabelle ⋮ 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 ⋮ A simple proof of a simple consensus algorithm ⋮ Generate & Check Method for Verifying Transition Systems in CafeOBJ ⋮ Factorizing fault tolerance. ⋮ 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 ⋮ A compositional framework for fault tolerance by specification transformation ⋮ 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 ⋮ A principle for sequential reasoning about distributed algorithms ⋮ 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 ⋮ Cones and foci: A mechanical framework for protocol verification ⋮ Foundations for using linear temporal logic in Event-B refinement ⋮ A mechanical proof of Segall's PIF algorithm ⋮ Formal and incremental construction of distributed algorithms: on the distributed reference counting algorithm ⋮ A basic algebra of stateless connectors ⋮ A verifiable low-level concurrent programming model based on colored Petri nets ⋮ Parallel elementwise processable functions in concurrent clean ⋮ A methodology for designing proof rules for fair parallel programs ⋮ Petri net based verification of distributed algorithms: An example ⋮ A predicate transformer for the progress property `to-always'
This page was built for software: UNITY