Dear all,
The next talk in the IARCS Verification Seminar Series will be given by
Azadeh Farzan, a Professor in the Computer Science Department of University
of Toronto. The talk is scheduled on Tuesday, April 02, at 1900 hrs IST (add
to Google calendar
<https://calendar.google.com/calendar/event?action=TEMPLATE&tmeid=NGxmbmFvYX…>
).
The details of the talk can be found on our 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,
Akash, Deepak, Madhukar, Srivathsan
=============================================================
Title: Coarser Equivalences for Causal Concurrency
Meeting Link:
https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09
(Meeting ID: 891 6409 4870, Passcode: 082194)
Abstract:
In this talk, I will discuss relaxations of trace equivalence with the goal
of maintaining its algorithmic advantages. Specifically, for the problem of
checking, in a streaming setting, if two arbitrary steps of a concurrent
program run are causally concurrent (i.e. they can be reordered in an
equivalent run) or causally ordered (i.e. they always appear in the same
order in all equivalent runs), trace equivalence yields constant-space
algorithms. I will discuss how certain relaxations, provably, do not yield
similar efficient algorithms. Then, I will introduce a new
commutativity-based notion of equivalence called grain equivalence that is
strictly more relaxed than trace equivalence, and yet yields a constant
space algorithm for the same problem. This notion of equivalence uses
commutativity of grains, which are sequences of atomic steps, in addition
to the standard commutativity from trace theory. I will discuss two
distinct cases when the grains are contiguous subwords of the input program
run and when they are not, formulate the precise definition of causal
concurrency in each case, and show that they can be decided in constant
space, despite being strict relaxations of the notion of causal concurrency
based on trace equivalence.
Bio: Azadeh Farzan is a Professor in the Computer Science Department of
University of Toronto. She received her PhD from the University of Illinois
at Urbana-Champaign. Her interests are in Software Verification,
Programming Languages, Formal Methods, and Security, with an emphasis on
concurrency-related issues.
