[FM-India] IARCS Verification Seminar Series -- Talk by Ramanathan Thinniyam on February 1, 1900 hrs IST

[VSS IARCS]

Dear all,

The next talk in the IARCS Verification Seminar Series will be given by
Ramanathan Thinniyam, a postdoc at the Max Planck Institute for Software
Systems at Kaiserslautern, Germany. The talk is scheduled on Tuesday,
February 1, at 1900 hrs IST (add to calendar
<https://fmindia.cmi.ac.in/vss/cal/vss-1Feb2022.ics>:
https://fmindia.cmi.ac.in/vss/cal/vss-1Feb2022.ics).

The details of the talk can be found on the webpage (
https://fmindia.cmi.ac.in/vss/), and also appended to the body of this
email.

The Verification Seminar Series, an initiative by the Indian Association
for Research in Computing Science (IARCS), is a monthly, online
talk-series, broadly in the area of Formal Methods and Programming
Languages, with applications in Verification and Synthesis. The aim of this
talk-series is to provide a platform for Formal Methods researchers to
interact regularly. In addition, we hope that it will make it easier for
researchers to explore newer problems/areas and collaborate on them, and
for younger researchers to start working in these areas.

All are welcome to join.


Best regards,
Deepak, Madhukar, Rahul, Srivathsan

=============================================================

Title: Context-bounded liveness verification of multithreaded shared-memory
programs

Meeting Link:
https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09
(Meeting ID: 891 6409 4870, Passcode: 082194)

Abstract: We study context-bounded verification of liveness properties of
multi-threaded, shared-memory programs, where each thread can spawn
additional threads. Our main result shows that context-bounded fair
termination is decidable for the model; context-bounded implies that each
spawned thread can be context switched a fixed constant number of times.
Our proof is technical, since fair termination requires reasoning about the
composition of unboundedly many threads each with unboundedly large stacks.
In fact, techniques for related problems, which depend crucially on
replacing the pushdown threads with finite-state threads, are not
applicable. Instead, we introduce an extension of vector addition systems
with states (VASS), called VASS with balloons (VASSB), as an intermediate
model; it is an infinite-state model of independent interest. A VASSB
allows tokens that are themselves markings (balloons). We show that context
bounded fair termination reduces to fair termination for VASSB. We show the
latter problem is decidable by showing a series of reductions: from fair
termination to configuration reachability for VASSB and thence to the
reachability problem for VASS. For a lower bound, fair termination is known
to be non-elementary already in the special case where threads run to
completion (no context switches).