Commutativity for concurrent program termination proofs

DOI10.1007/978-3-031-37706-8_6MaRDI QIDQ6535630zbMATH OpenFDO

Authors Danya Lette, Azadeh Farzan

Publication date 1 February 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-37706-8_6

Mathematics Subject Classification ID

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

Recommendations

• Transition invariants and transition predicate abstraction for program termination
• Local Proofs for Linear-Time Properties of Concurrent Programs
• Automata-Based Termination Proofs
• Streamlining progress-based derivations of concurrent programs
• Convergence: integrating termination and abort-freedom

Cites work

• A calculus of atomic actions
• Automated hypersafety verification
• Compositional termination proofs for multi-threaded programs
• Layered concurrent programs
• Linear ranking for linear lasso programs
• Local Proofs for Linear-Time Properties of Concurrent Programs
• Local temporal reasoning
• Partial-order methods for the verification of concurrent systems. An approach to the state-explosion problem
• Precise Thread-Modular Verification
• Proving LTL Properties of Bitvector Programs and Decompiled Binaries
• Proving liveness of parameterized programs
• Proving non-termination
• Reduction
• Rely-guarantee bound analysis of parameterized concurrent shared-memory programs. With an application to proving that non-blocking algorithms are bounded lock-free
• The MathSAT5 SMT solver
• Transition invariants and transition predicate abstraction for program termination
• Ultimately periodic words of rational ω-languages

Cited in

(1)

• Choose your proofs: commutativity and symmetry for smarter reasoning

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

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