Context-Bounded Verification of Liveness: D Proofs for Section 5.3
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
D PROOFS FOR SECTION 5.3
The proofs of Lemmas 5.4 and 5.5 both assume that the VASSB considered is both zero-base (by Lemma C.7) and typed (by Lemma C.6). Further, the notion of runs-with-id introduced in Appendix C is used in the proof of Lemma 5.4.
D.1 Proof of Lemma 5.4
D.2 Proof of Lemma 5.5
L O A D I N G
. . . comments & more!
. . . comments & more!
