UNITY

swMATH13461MaRDI QIDQ25375FDOQ25375

Author name not available (Why is that?)

Described by source

• Simulation model development and analysis in UNITY
• Unnamed Publication

Cited In (only showing first 100 items - show all)

• Tiara: a self-stabilizing deterministic skip list and skip graph
• A walk over the shortest path: Dijkstra's algorithm viewed as fixed-point computation.
• Credible execution of bounded-time parallel systems with delayed diagnosis
• A framework for automated distributed implementation of component-based models
• Another glance at the Alpern-Schneider characterization of safety and liveness in concurrent executions
• Unity properties and sequences of states, some observations
• Queue based mutual exclusion with linearly bounded overtaking
• Distributed consensus, revisited
• A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic
• Splitting atoms safely
• Abstract compositional analysis of iterated relations. A structural approach to complex state transition systems
• Event-based proof of the mutual exclusion property of Peterson's algorithm
• Simulation refinement for concurrency verification
• A queue based mutual exclusion algorithm
• Theories for mechanical proofs of imperative programs
• Partial correctness for probabilistic demonic programs
• DUALITY: A simple formalism for the analysis of UNITY
• Mechanizing a process algebra for network protocols
• Cones and foci: A mechanical framework for protocol verification
• Modeling adaptive behaviors in Context UNITY
• Fixed points of increasing functions
• A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
• Verification of distributed systems with local-global predicates
• Progress properties for empty \textsc{Unity} programs
• The chemical abstract machine
• Focus points and convergent process operators: A proof strategy for protocol verification
• Property preserving abstractions for the verification of concurrent systems
• A compositional framework for fault tolerance by specification transformation
• Parallel elementwise processable functions in concurrent clean
• Generic systolic arrays: A methodology for systolic design
• Stabilizing phase-clocks
• Correctness and concurrent complexity of the black-white bakery algorithm
• A framework for viewing atomic events in distributed computations
• Abstract state machines: a unifying view of models of computation and of system design frameworks
• An incremental specification of the sliding-window protocol
• Phase synchronization
• Safety and liveness from a methodological point of view
• Concurrent maintenance of rings
• A basic algebra of stateless connectors
• Ensuring completeness of symbolic verification methods for infinite-state systems
• Convergence of iteration systems
• Starvation-free mutual exclusion with semaphores
• The distributed simulation of clustered processes
• A fixed point approach to parallel discrete event simulation
• Foundations for using linear temporal logic in Event-B refinement
• Refinement verification of the lazy caching algorithm
• A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
• Knowledge-Based Synthesis of Distributed Systems Using Event Structures
• Superposition refinement of reactive systems
• Knowledge-based programs
• Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous
• A verification framework for agent programming with declarative goals
• A verifiable low-level concurrent programming model based on colored Petri nets
• Structural transformations for data-enriched real-time systems
• Compositional Verification for Component-Based Systems and Application
• A simple proof of a simple consensus algorithm
• Application of the composition principle to unity-like specifications
• Composite registers
• Transformation of programs for fault-tolerance
• A fast, scalable mutual exclusion algorithm
• Probabilistic communicating processes
• Linda-based applicative and imperative process algebras
• Conditional rewriting logic as a unified model of concurrency
• Generate & Check Method for Verifying Transition Systems in CafeOBJ
• Theorem Proving Based on Proof Scores for Rewrite Theory Specifications of OTSs
• Maintaining the Ranch topology
• A principle for sequential reasoning about distributed algorithms
• Adaptive solutions to the mutual exclusion problem
• Title not available (Why is that?)
• A simplified design strategy for mapping image processing algorithms on a SIMD torus
• An experiment with the use of predicate transformers in UNITY
• On the implementation of concurrent calculi in net calculi: two case studies
• On the logic of UNITY
• A Rewriting-Based Model Checker for the Linear Temporal Logic of Rewriting
• A general technique for proving lock-freedom
• Eliminating the substitution axiom from UNITY logic
• Computing with multiple discrete flows
• Web Cube
• Wait-free linearization with an assertional proof
• An Algebraic Approach to Refinement with Fair Choice
• Factorizing fault tolerance.
• Wait-free linearization with a mechanical proof
• A case study in transformational design of concurrent systems
• Quantitative program logic and expected time bounds in probabilistic distributed algorithms.
• The shortest path in parallel
• Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL
• UNITY and Büchi automata
• Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols
• Some impossibility results in interprocess synchronization
• A Normalized Form for FIFO Protocols Traces, Application to the Replay of Mode-based Protocols
• Interfaces between languages for communicating systems
• Reasoning about programs by exploiting the environment
• Alternating states for dual nondeterminism in imperative programming
• A new explanation of the glitch phenomenon
• Specification and verification of concurrent programs through refinements
• Towards a Combination of CafeOBJ and PAT
• Formal verification of a programming logic for a distributed programming language
• Mechanizing UNITY in Isabelle
• Mapping PUNITY to UniNet
• Linearization in parallel pCRL

This page was built for software: UNITY