A foundation for modular reasoning about safety and progress properties of state-based concurrent programs
From MaRDI portal
Publication:1391101
DOI10.1016/S0304-3975(96)00327-1zbMath0901.68034MaRDI QIDQ1391101
Publication date: 22 July 1998
Published in: Theoretical Computer Science (Search for Journal in Brave)
68N99: Theory of software
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- On using temporal logic for refinement and compositional verification of concurrent systems
- Unity properties and sequences of states, some observations
- Eliminating the substitution axiom from UNITY logic
- P-A logic - a compositional proof system for distributed programs
- The existence of refinement mappings
- A predicate transformer for progress
- Compositionality, Concurrency and Partial Correctness. Proof Theories for Networks of Processes, and their Relationship
- Derivation of concurrent programs: Two examples
- Composition of assumption-commitment specifications in a UNITY style
- Predicate transformers for reasoning about concurrent computation
- Invariants, composition, and substitution
- DUALITY: A simple formalism for the analysis of UNITY
- Proofs of Networks of Processes
- Logical foundations for compositional verification and development of concurrent programs in UNITY