Adequate proof principles for invariance and liveness properties of concurrent programs

DOI10.1016/0167-6423(84)90003-0MaRDI QIDQ795497zbMATH OpenOpenAlexFDO

Authors Zohar Manna, Amir Pnueli

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

zbMATH Keywords

concurrent programsinvariance propertiesliveness properties

Mathematics Subject Classification ID

Theory of operating systems (68N25)

Recommendations

• Concurrent program verification with invariant-guided underapproximation
• Specification and verification of concurrent programs through refinements
• scientific article; zbMATH DE number 177266
• On verifying that a concurrent program satisfies a nondeterministic specification
• A proof system for concurrent ADA programs
• Property preserving abstractions for the verification of concurrent systems

Cited in

(29)

• Atomic semantics of nonatomic programs
• The power of temporal proofs
• An operator net model for distributed systems
• Completing the temporal picture
• 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
• A formal model of asynchronous communication and its use in mechanically verifying a biphase mark protocol
• Proving partial order properties
• A mechanically verified incremental garbage collector
• A methodology for designing proof rules for fair parallel programs
• On relative and probabilistic finite counterability
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• Verification of concurrent programs: The automata-theoretic framework
• Interleaving set temporal logic
• Property Directed Reachability for Proving Absence of Concurrent Modification Errors
• Syntax directed analysis of liveness properties of while programs
• 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
• Proving liveness of parameterized programs
• Quantitative safety and liveness
• Liminf progress measures
• Using partial orders for the efficient verification of deadlock freedom and safety properties
• Automated temporal reasoning about reactive systems
• A complete fragment of LTL(EB)
• Compositional transformational design for concurrent programs
• Verifying atomic data types

This page was built for publication: Adequate proof principles for invariance and liveness properties of concurrent programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q795497)