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
