Context-Bounded Verification of Liveness: C Proofs for Section 5

Written by multithreading | Published 2024/03/15
Tech Story 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

TLDRWe study context-bounded verification of liveness properties of multi-threaded, shared-memory programs, where each thread can spawn additional threads.via the TL;DR App

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

C PROOFS FOR SECTION 5

C.1 Proof of Lemma 5.1

C.2 Proof of Lemma 5.3

Written by multithreading | Research to enable more than one user at a time without requiring multiple copies of the program running on the computer
Published by HackerNoon on 2024/03/15
ABOUTHow hackers start their afternoons. We publish tech stories and build publishing software.

READEntirely free library read by hundreds of millions to learn anything about any technology.

WRITEHackerNoon elevates quality technology writing far and wide across the interwebs.

PARTNERHackerNoon works directly with tech companies to place ads by content relevancy