A methodology for designing proof rules for fair parallel programs

DOI10.1007/BF01211296zbMath0889.68101MaRDI QIDQ1377299

J. Ning

Publication date: 11 June 1998

Published in: Formal Aspects of Computing (Search for Journal in Brave)

zbMATH Keywords

formal semanticstemporal logicprogram correctness

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Semantics in the theory of computing (68Q55)

Uses Software

• UNITY

Cites Work

• Adequate proof principles for invariance and liveness properties of concurrent programs
• Fair termination revisited - with delay
• Defining liveness
• The \(\mu\)-calculus as an assertion-language for fairness arguments
• Modalities for model checking: Branching time logic strikes back
• A proof rule for fair termination of guarded commands
• Countable nondeterminism and random assignment
• Ten Years of Hoare's Logic: A Survey—Part I
• Proving Liveness Properties of Concurrent Programs
• Guarded commands, nondeterminacy and formal derivation of programs
• Verifying properties of parallel programs
• Formal verification of parallel programs
• A New Incompleteness Result for Hoare's System
• Soundness and Completeness of an Axiom System for Program Verification
• An axiomatic basis for computer programming
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item