Verification of Concurrent Programs under Release Acquire

Shibashis Guha
Tuesday, 5 Mar 2024, 16:00 to 17:00
A-201 (STCS Seminar Room)

This is an overview of some recent work on the verification of concurrent programs. Traditionally concurrent programs are interpreted under sequential consistency (SC). Even though SC is very intuitive and easy to use, modern multiprocessors  do not employ SC for performance reasons, and instead use so called "weak memory models".  Some of the well known weak memory  models in vogue are  Intel x-86, IBM POWER and ARM.  Weak memory features are also incorporated in the development of modern programming languages  such as C11 and Java. This talk is on the verification of concurrent programs under the release acquire (RA) semantics, with the main focus being on decidability and complexity questions.

Short Bio:

Krishna is a faculty member in the department of computer science and engineering at IIT Bombay. Her areas of research are automata theory, logics, and their applications to the verification of quantitative as well as distributed/concurrent  systems.