FMIndia

Download

fmindia@cmi.ac.in

April 2024

5 participants
11 discussions

IARCS Verification Seminar Series -- Talk by Azadeh Farzan on April 2 at 1900 hrs IST
by VSS IARCS 01 Apr '24

01 Apr '24

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.

1 0