Short CV: Madhavan Mukund studied at IIT Bombay (BTech) and Aarhus University (Ph.D.). He has been a faculty member at Chennai Mathematical Institute since 1992, where he is presently Professor and Dean of Studies. His main research area is formal verification. He has active collaborations within and outside India and regularly serves on international conference programme committees.
He is President of the Indian Association for Research in Computing Science (IARCS) and Vice President of the ACM India Council. He enjoys teaching. He has been the National Coordinator of the Indian Computing Olympiad since 2002 and was Executive Director of the International Olympiad in Informatics from 2011 to 2014.
Title of Talk 1: Automata and Program Verification
Synopsis: The finite-state automaton model is a very useful abstraction that allows us to capture essential features of a computational system. The language of temporal logic allows us to make assertions about the executions of such finite-state systems. Typically, these assertions are combinations of safety properties ("nothing bad happens") and liveness properties ("something good eventually happens"). These temporal requirements can then be checked algorithmically with respect to the given finite-state automaton model of the underlying system. This process is called model-checking.
In this talk, we introduce the central ideas involved in model-checking. We show how to model a program as a finite-state system, we introduce the language of temporal logic and we describe the algorithmic process for verifying assertions in temporal logic.
Title of Talk 2: Concurrent Programming: Old Problems, New Challenges
Synopsis: Concurrency has generally been the domain of specialist programmers well-versed in the use of tools such as locks, semaphores and monitors for tackling slippery problems like data inconsistency and race conditions. However, with the advent of multicore processors and large scale distributed applications, it is becoming harder to avoid dealing with these issues on a day-to-day basis.
In this talk, we examine interesting challenges at both ends of the spectrum. At the processor level, we look at how relaxed memory models, designed to optimize sequential code, create unexpected problems for concurrent programs. At the network level, we describe a weakened notion of data consistency called eventual consistency that has been introduced to deal with distributed objects such as Facebook like counters and Amazon shopping carts.
Qualifications: BTech (CSE), Ph.D. (CS)
Title: Professor and Dean of Studies
Affiliation: Chennai Mathematical Institute
Contact Details: firstname.lastname@example.org