Commutativity for concurrent program termination proofs

DOI10.1007/978-3-031-37706-8_6zbMath1547.68125MaRDI QIDQ6535630

Azadeh Farzan, Danya Lette

Publication date: 1 February 2024

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• Compositional Termination Proofs for Multi-threaded Programs
• Transition Invariants and Transition Predicate Abstraction for Program Termination
• Proving non-termination
• Local Proofs for Linear-Time Properties of Concurrent Programs
• Precise Thread-Modular Verification
• Reduction
• Local temporal reasoning
• Proving Liveness of Parameterized Programs
• Linear Ranking for Linear Lasso Programs
• A calculus of atomic actions
• The MathSAT5 SMT Solver
• Ultimately periodic words of rational ω-languages
• Layered concurrent programs
• Automated hypersafety verification
• Proving LTL Properties of Bitvector Programs and Decompiled Binaries

This page was built for publication: Commutativity for concurrent program termination proofs