Context-Bounded Verification of Liveness: C Proofs for Section 5
by MultiThreading.Tech: #1 Publication on Concurrent ProgrammingMarch 15th, 2024
Too Long; Didn't Read
We study context-bounded verification of liveness properties of multi-threaded, shared-memory programs, where each thread can spawn additional threads.
This paper is available on arxiv under CC BY-NC-SA 4.0 DEED license.
Authors:
(1) Pascal Baumann, Max Planck Institute for Software Systems (MPI-SWS), Germany;
(2) Rupak Majumdar, Max Planck Institute for Software Systems (MPI-SWS), Germany;
(3) Ramanathan S. Thinniyam, Max Planck Institute for Software Systems (MPI-SWS), Germany;
(4) Georg Zetzsche, Max Planck Institute for Software Systems (MPI-SWS), Germany.
Table of Links
- Introduction
- Dynamic Networks of Concurret Pushdown Systems (DCPS)
- Warm-up: Non-Termination
- Fair Non-Termination
- From Progressive Runs for VASSB to Reachability
- Starvation
- Conclusion, Acknowledgment & References
- A. Strengthening Fairness to Progressive Runs
- B. Proofs from Section 4.1
- C. Proofs for Section 5
- D. Proofs for Section 5.3
- E. Proofs for Section 6
C PROOFS FOR SECTION 5
C.1 Proof of Lemma 5.1
C.2 Proof of Lemma 5.3
L O A D I N G
. . . comments & more!
. . . comments & more!
