The following pages link to UNITY (Q25375):
Displaying 50 items.
- Comments on ''Always-true is not invariant'': Assertional reasoning about invariance (Q1183477) (← links)
- A simple proof of a completeness result for \(leads\)-\(to\) in the UNITY logic (Q1186571) (← links)
- Tuning distributed control algorithms for optimal functioning (Q1187845) (← links)
- Weakest preconditions for progress (Q1189258) (← links)
- The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\) (Q1190479) (← links)
- Conditional rewriting logic as a unified model of concurrency (Q1190488) (← links)
- The chemical abstract machine (Q1190491) (← links)
- Credible execution of bounded-time parallel systems with delayed diagnosis (Q1192010) (← links)
- A compositional protocol verification using relativized bisimulation (Q1193593) (← links)
- Operational specification with joint actions: Serializable databases (Q1193603) (← links)
- Specifying modules to satisfy interfaces: A state transition system approach (Q1193606) (← links)
- Efficient algorithms for parallel sorting on mesh multicomputers (Q1193763) (← links)
- Transformation of programs for fault-tolerance (Q1201297) (← links)
- A verification system for concurrent programs based on the Boyer-Moore prover (Q1203115) (← links)
- Machine checked proofs of the design of a fault-tolerant circuit (Q1203129) (← links)
- Some impossibility results in interprocess synchronization (Q1261111) (← links)
- Fairness and hyperfairness in multi-party interactions (Q1261113) (← links)
- Theories for mechanical proofs of imperative programs (Q1267030) (← links)
- Program construction by verifying specification (Q1273080) (← links)
- Abstract compositional analysis of iterated relations. A structural approach to complex state transition systems (Q1276498) (← links)
- Formal verification of a programming logic for a distributed programming language (Q1285659) (← links)
- Symbolic verification method for definite iteration over data structures (Q1285767) (← links)
- Convergence of iteration systems (Q1310569) (← links)
- Models for the substitution axiom of UNITY logic (Q1313738) (← links)
- A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol (Q1318283) (← links)
- Eliminating disjunctions of leads-to properties (Q1318740) (← links)
- Program refinement in fair transition systems (Q1323314) (← links)
- Axiomatic-like performance analysis (ALPA) (Q1324358) (← links)
- A compositional framework for fault tolerance by specification transformation (Q1330423) (← links)
- Program composition via unification (Q1331925) (← links)
- Correct translation of data parallel assignment onto array processors (Q1336950) (← links)
- Error in the UNITY substitution rule for subscripted operators (Q1336953) (← links)
- Properties of concurrent programs (Q1346603) (← links)
- A principle for sequential reasoning about distributed algorithms (Q1346611) (← links)
- Property preserving abstractions for the verification of concurrent systems (Q1346649) (← links)
- Focus points and convergent process operators: A proof strategy for protocol verification (Q1349249) (← links)
- Verifying a distributed list system: A case history (Q1355754) (← links)
- A mechanical proof of Segall's PIF algorithm (Q1362774) (← links)
- A methodology for designing proof rules for fair parallel programs (Q1377299) (← links)
- Petri net based verification of distributed algorithms: An example (Q1377301) (← links)
- A predicate transformer for the progress property `to-always' (Q1377323) (← links)
- A foundation for modular reasoning about safety and progress properties of state-based concurrent programs (Q1391101) (← links)
- Formal verification of a leader election protocol in process algebra (Q1391796) (← links)
- Almost-certain eventualities and abstract probabilities in the quantitative temporal logic qTL (Q1395428) (← links)
- Mapping PUNITY to UniNet (Q1415945) (← links)
- Computing left Kan extensions. (Q1426132) (← links)
- Linda-based applicative and imperative process algebras (Q1575260) (← links)
- Simplification of boolean verification conditions (Q1575276) (← links)
- Composing leads-to properties (Q1575647) (← links)
- Quantitative program logic and expected time bounds in probabilistic distributed algorithms. (Q1603711) (← links)
