• Home
• Newsletters
• People of ACM
• People of ACM - Madhavan Mukund

People of ACM - Madhavan Mukund

April 26, 2018

How did you become interested in the theoretical side of computer science?

After I graduated from IIT Bombay, I joined a government-funded organization for software development that had been spawned from the Tata Institute of Fundamental Research (TIFR). I stayed on campus at TIFR and spent many enjoyable evenings in the company of senior PhD students. The discussions I had with them sparked my interest in theoretical computer science and they convinced me I should switch tracks and start a PhD in this area.

You have said that young people have been moving away from India’s rich tradition in mathematics. How have the activities of Chennai Mathematical Institute aided in their return to the field?

Post 1950, there was a conscious policy in India to set up specialized research institutes in different areas, disconnected from the universities. Good faculty tended to gravitate to these institutions, leaving a void in the universities. This, coupled with the increasing attractiveness of engineering courses, led to a drastic decline in interest and enrolment in programs offering basic sciences and mathematics. CMI’s decision to start an undergraduate program in 1998 was aimed at reversing this trend by bringing active research mathematicians back in contact with young students. Though the program is very small in scale, especially in an Indian context, it has produced a number of excellent researchers in mathematics and computer science, several of whom are now faculty members at leading academic institutions in India. CMI’s example has also led other institutions to start similar program. It is still difficult to convince talented students to abandon engineering for mathematics. A lot remains to be done to spread awareness about career opportunities related to mathematics. However, without CMI’s intervention, the slow process of change that is currently taking place would have been further delayed, and even less effective.

You have been working in the area of automata-theoretic models. Can you tell us a little about the role these models can play in formal verification?

In traditional science and engineering, it is well accepted that we understand complex natural and physical phenomena through mathematical models that abstract away inessential details. Computational systems, whether software or hardware, are already constructed through a process of abstraction, so it is less evident that we need to build mathematical models to understand them. Computability theory tells us that fully automated verification is impossible, but we can achieve a lot through judicious simplification. Automata are natural models for traditional discrete state systems. By focusing on the relevant features, we can often reduce complicated systems to either finite-state devices or pushdown systems for which we have effective algorithms to compute reachable states and other properties.

This kind of model building is particularly important for concurrent and distributed systems that exhibit complex behaviors due to asynchronous interleaving of the components. Testing all possible runs is impossible due to the combinatorial explosion of effort, and bugs observed in practice are often difficult or impossible to reproduce. With a mathematical model, we can explore all possible behaviors more effectively and validate whether such a system is free of errors, especially bugs that arise from unforeseen interactions between components.

What is an area of research that you think holds special promise in improving the overall effectiveness of modeling systems?

Traditionally, formal verification has built models based on finite-state automata or pushdown systems. However, modern computational systems combine discrete and continuous behavior. Examples include fly-by-wire software in planes and controllers for nuclear plants. These safety-critical systems are now deployed in devices closer to home, like automobiles and medical implants. To verify such systems, we need to build richer models and check a wider range of properties.

Timed and hybrid automata are steps in this direction, but decidable fragments are very limited and the computational complexity of analysis is high. There is a rich history of using stochastic models and systems described using partial differential equations in areas such as control theory. We need to embrace these aspects in our models. We also need to understand and exploit constraints in the systems being modeled to make models simpler and analysis more tractable. Finally, given that modern devices are highly instrumented and produce large volumes of diagnostic data, we can apply machine learning to discover anomalous behavior. All of these aspects are already being explored by various research groups, but it is difficult to find people or even groups with expertise across these areas.

Another key point for formal verification to become more widespread is to recognize that building formal models is a time and labor-intensive task, and hence expensive. A couple of years ago, I heard a talk by J Strother Moore where he said that this effort should be compared to the cost of rebuilding the system from scratch using a team with no prior experience.  Companies are beginning to realize that their overall cost does decrease if they invest in this effort as part of their development process. So using formal methods to specify and build systems leads to savings in the long run, because these formal specifications lead to more effective model building for analysis.

Your term as President of the ACM India Council runs through the end of June 2018. What were some initiatives that were launched or expanded during your tenure as President? What have you enjoyed most about your work with the ACM India Council?

One of the key areas where we hope to make an impact through ACM India is in computer science education. The original focus was at the university level, but in 2016 we embarked on a new program called CSpathshala to take computational thinking to schools.  CSpathshala has succeeded beyond our most optimistic expectations.  We have 150+ schools and 100,000 students participating in pilot programs. We are also working with some government agencies to deploy our curriculum in state run schools.

A major hurdle to influencing education policy is to be recognized by government agencies and other stakeholders as a credible partner. During the past year, we have seen this happening. As I mentioned earlier, some government agencies are adopting CSpathshala material. ACM India has become formally involved in curriculum design and textbook writing for the major national level school board. We have also been invited by the national body that coordinates engineering education across India to contribute to the revision of the computer science curriculum.

These efforts have brought me, in particular, and ACM India, in general, in contact with a large pool of enthusiastic volunteers, both from academia and industry. Their level of energy and engagement brings new dynamism to ACM India’s efforts and gives me great hope that we can make a tangible difference, despite the magnitude of the tasks we have set ourselves.