A foundation for modular reasoning about safety and progress properties of state-based concurrent programs

DOI10.1016/S0304-3975(96)00327-1zbMath0901.68034MaRDI QIDQ1391101

Edgar Knapp, Pierre Collette

Publication date: 22 July 1998

Published in: Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

UNITY programs

Mathematics Subject Classification ID

Theory of software (68N99)

Related Items

UNITY and Büchi automata

Uses Software

• UNITY

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