Adequate proof principles for invariance and liveness properties of concurrent programs
From MaRDI portal
Publication:795497
DOI10.1016/0167-6423(84)90003-0zbMath0542.68014OpenAlexW2039025680MaRDI QIDQ795497
Publication date: 1984
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0167-6423(84)90003-0
Related Items
A mechanically verified incremental garbage collector ⋮ Interleaving set temporal logic ⋮ Atomic semantics of nonatomic programs ⋮ The power of temporal proofs ⋮ A methodology for designing proof rules for fair parallel programs ⋮ An operator net model for distributed systems ⋮ Méthode axiomatique sur les propriétés de fatalité des programmes parallèles ⋮ Temporal predicate transition nets—a new formalism for specifying and verifying concurrent systems ⋮ Quantitative safety and liveness ⋮ Liminf progress measures ⋮ Verifying atomic data types ⋮ Completing the temporal picture ⋮ On relative and probabilistic finite counterability ⋮ A criterion for atomicity ⋮ Specifying modules to satisfy interfaces: A state transition system approach ⋮ Axiomatic treatment of processes with shared variables revisited ⋮ Defining conditional independence using collapses ⋮ A verification system for concurrent programs based on the Boyer-Moore prover ⋮ Verification of concurrent programs: The automata-theoretic framework ⋮ Using partial orders for the efficient verification of deadlock freedom and safety properties ⋮ A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol ⋮ Proving partial order properties
