Compositional termination proofs for multi-threaded programs

DOI10.1007/978-3-642-28756-5_17MaRDI QIDQ2894275zbMATH OpenOpenAlexFDO

Authors Andrey Rybalchenko, C. Popeea

Publication date 29 June 2012

Published in Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-28756-5_17

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Proof spaces for unbounded parallelism
• Compositional verification of termination-preserving refinement of concurrent programs
• Abstract threads
• Predicate abstraction and refinement for verifying multi-threaded programs
• scientific article; zbMATH DE number 176727

Cited in

(9)

• Termination and cost analysis of loops with concurrent interleavings
• Towards a thread-local proof technique for starvation freedom
• Compositional verification of termination-preserving refinement of concurrent programs
• May-happen-in-parallel analysis for actor-based concurrency
• Multithreaded-Cartesian abstract interpretation of multithreaded recursive programs Is polynomial
• Interactive Termination Proofs Using Termination Cores
• Rely-guarantee termination and cost analyses of loops with concurrent interleavings
• Thread-modular counter abstraction: automated safety and termination proofs of parameterized software by reduction to sequential program verification
• Commutativity for concurrent program termination proofs

This page was built for publication: Compositional termination proofs for multi-threaded programs

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