UNITY
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A general technique for proving lock-freedom
- Refinement and verification in component-based model-driven design
- A queue based mutual exclusion algorithm
- Boolean circuit programming: A new paradigm to design parallel algorithms
- Refining multiset transformers
- A framework for viewing atomic events in distributed computations
- An incremental specification of the sliding-window protocol
- Phase synchronization
- Comments on Always-true is not invariant: Assertional reasoning about invariance
- A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic
- Tuning distributed control algorithms for optimal functioning
- Weakest preconditions for progress
- The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\)
- Conditional rewriting logic as a unified model of concurrency
- The chemical abstract machine
- Credible execution of bounded-time parallel systems with delayed diagnosis
- A compositional protocol verification using relativized bisimulation
- Operational specification with joint actions: Serializable databases
- Specifying modules to satisfy interfaces: A state transition system approach
- Efficient algorithms for parallel sorting on mesh multicomputers
- Transformation of programs for fault-tolerance
- A verification system for concurrent programs based on the Boyer-Moore prover
- Machine checked proofs of the design of a fault-tolerant circuit
- Some impossibility results in interprocess synchronization
- Fairness and hyperfairness in multi-party interactions
- Theories for mechanical proofs of imperative programs
- Program construction by verifying specification
- Abstract compositional analysis of iterated relations. A structural approach to complex state transition systems
- Formal verification of a programming logic for a distributed programming language
- Symbolic verification method for definite iteration over data structures
- D-Finder
- Convergence of iteration systems
- Models for the substitution axiom of UNITY logic
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
- Eliminating disjunctions of leads-to properties
- Program refinement in fair transition systems
- Axiomatic-like performance analysis (ALPA)
- A compositional framework for fault tolerance by specification transformation
- Program composition via unification
- Correct translation of data parallel assignment onto array processors
- Error in the UNITY substitution rule for subscripted operators
- 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
- SCADE
- A mechanical proof of Segall's PIF algorithm
- 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'
- A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
- Formal verification of a leader election protocol in process algebra
- Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL
- TIMES
- Mapping PUNITY to UniNet
- rCOS
- Computing left Kan extensions.
- ConGolog
- LARCH
- HOL/SPIN
- BETA
- Linda-based applicative and imperative process algebras
- Simplification of boolean verification conditions
- Composing leads-to properties
- POOL
- TRAM
- TCOZ
- Quantitative program logic and expected time bounds in probabilistic distributed algorithms.
- A walk over the shortest path: Dijkstra's algorithm viewed as fixed-point computation.
- The shortest path in parallel
- Tournaments for mutual exclusion: verification and concurrent complexity
- Simulation relations for fault-tolerance
- OBJ3
- Abstract state machines: a unifying view of models of computation and of system design frameworks
- Specification and analysis of a composition of protocols
- The sliding-window protocol revisited
- A simple proof of a simple consensus algorithm
- AgentSpeak
- Reo
- Factorizing fault tolerance.
- Invariants, composition, and substitution
- Bounded delay for a free address
- Kumo
- 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
- Rodin
- B4Free
- Superposition refinement of reactive systems
- A framework for automated distributed implementation of component-based models
- Using refinement calculus techniques to prove linearizability
- Security invariants in discrete transition systems
- Concurrent maintenance of rings
- NQTHM
- Formalism and method
- UNITY and Büchi automata
- fireLib
- BEHAVE
- Linda
This page was built for software: UNITY
