TL;DR —
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
[story continues]
Written by
@multithreading
Research to enable more than one user at a time without requiring multiple copies of the program running on the computer
Topics and
tags
tags
liveness-verification|multi-threaded-memory-programs|shared-memory-programs|vector-addition-systems|vass-with-balloons|context-bounded-verification|multithreaded-shared-memory|multi-pushdown-systems
This story on HackerNoon has a decentralized backup on Sia.
Transaction ID: nFfTQLoZZ1yIEnmwyz8FwxCKLUHIst2nA0HnFnH0P90