UNITY
From MaRDI portal
Cited in
(only showing first 100 items - show all)- Conditional rewriting logic: Deduction, models and concurrency
- Eliminating the substitution axiom from UNITY logic
- Web Cube
- Tiara: a self-stabilizing deterministic skip list and skip graph
- Credible execution of bounded-time parallel systems with delayed diagnosis
- A walk over the shortest path: Dijkstra's algorithm viewed as fixed-point computation.
- Factorizing fault tolerance.
- Wait-free linearization with an assertional proof
- 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
- Wait-free linearization with a mechanical proof
- A case study in transformational design of concurrent systems
- Distributed consensus, revisited
- A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic
- 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
- Splitting atoms safely
- UNITY and Büchi automata
- Constructive polychronous systems
- Abstract compositional analysis of iterated relations. A structural approach to complex state transition systems
- Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols
- Event-based proof of the mutual exclusion property of Peterson's algorithm
- Simulation refinement for concurrency verification
- Some impossibility results in interprocess synchronization
- Generic proof scores for generate \& check method in CafeOBJ
- rCOS: defining meanings of component-based software architectures
- A queue based mutual exclusion algorithm
- Interfaces between languages for communicating systems
- Alternating states for dual nondeterminism in imperative programming
- Theories for mechanical proofs of imperative programs
- A new explanation of the glitch phenomenon
- Formal verification of a programming logic for a distributed programming language
- Specification and verification of concurrent programs through refinements
- Reasoning about programs by exploiting the environment
- Mapping PUNITY to UniNet
- Mechanizing UNITY in Isabelle
- Partial correctness for probabilistic demonic programs
- Generate \& check method for verifying transition systems in CafeOBJ
- DUALITY: A simple formalism for the analysis of UNITY
- Program construction by verifying specification
- Linearization in parallel pCRL
- Mechanizing a process algebra for network protocols
- Axiomatic-like performance analysis (ALPA)
- Cones and foci: A mechanical framework for protocol verification
- Constraining interference in an object-based design method
- Computing left Kan extensions.
- Modeling adaptive behaviors in Context UNITY
- Fixed points of increasing functions
- Verification of distributed systems with local-global predicates
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
- A verification system for concurrent programs based on the Boyer-Moore prover
- Formal and incremental construction of distributed algorithms: on the distributed reference counting algorithm
- Progress properties for empty \textsc{Unity} programs
- Symbolic verification method for definite iteration over data structures
- Refinement and verification in component-based model-driven design
- Knowledge-based synthesis of distributed systems using event structures
- The chemical abstract machine
- An algebraic approach to refinement with fair choice
- Refining multiset transformers
- A rewriting-based model checker for the linear temporal logic of rewriting
- Formal verification of a leader election protocol in process algebra
- Focus points and convergent process operators: A proof strategy for protocol verification
- Property preserving abstractions for the verification of concurrent systems
- Bounded delay for a free address
- Applying abstraction and formal specification in numerical software design
- Parallel elementwise processable functions in concurrent clean
- A compositional framework for fault tolerance by specification transformation
- Stabilizing phase-clocks
- Safety assurance via on-line monitoring
- Generic systolic arrays: A methodology for systolic design
- Correctness and concurrent complexity of the black-white bakery algorithm
- Distributed maximum maintenance on hierarchically divided graphs
- Temporal logic and fair discrete systems
- A framework for viewing atomic events in distributed computations
- Phase synchronization
- Abstract state machines: a unifying view of models of computation and of system design frameworks
- An incremental specification of the sliding-window protocol
- Using refinement calculus techniques to prove linearizability
- Safety and liveness from a methodological point of view
- Security invariants in discrete transition systems
- D-Finder
- SCADE
- rCOS
- TIMES
- ConGolog
- LARCH
- HOL/SPIN
- BETA
- POOL
- TRAM
- TCOZ
- OBJ3
- AgentSpeak
- Reo
- Kumo
- B4Free
- Rodin
This page was built for software: UNITY
