New faculty on the block: Govind R
December 15, 2025 | Bharti Dharapuram
Govind R recently joined IMSc as a faculty member in the Theoretical Computer Science group and his research focuses on formal methods. He has a PhD from the Université de Bordeaux and Chennai Mathematical Institute (CMI). He also has a Master’s degree from CMI, and completed his Bachelor’s degree from the National Institute of Technology (NIT), Calicut. He joins IMSc after postdoctoral research experience at Uppsala University and the Indian Institute of Technology, Bombay.
How did your interest in research develop?
My interest in research started with reading popular science books and science fiction. Thanks to my parents and grandfather, I read books about science, such as those by George Gamow, and the science magazines Eureka and Sasthragathi by the Kerala Sasthra Sahithya Parishad. During my childhood, I also got to spend three years at the Indian Institute of Science (IISc), Bangalore, where my father was doing his PhD. Interacting with his friends and participating in science club activities played an important role in giving me some perspective about science.
When I joined NIT Calicut for my undergraduate studies, a mentor, Prof Murali Krishnan, gave me a flavour of the different courses in theory. I also got to do internships at IISc and interacted with people there, which attracted me to theoretical computer science. At this point, I did not have much exposure to automata and formal verification methods, themes I work on currently. However, CMI has a substantial number of people working on these subjects who also teach courses, and that really helped me converge on these topics. CMI also sees many visitors from France every year, who offer courses and spend time there doing research. Working with one of them, Paul Gastin from Laboratoire Spécification et Vérification, ENS Paris-Saclay introduced me to research and how it is done.
What do you work on?
What I work on, broadly, is called formal methods, where the idea is to take a system and ensure that it behaves correctly at all times. The goal is to take systems from real life, typically software systems which are huge, and model them using automata-based models and state their specific properties, typically using logical specifications. Formal verification is where you take an automata model and a logical specification and ensure that the model is guaranteed to satisfy this specification. One way people did this earlier is by testing, where you try several inputs to check if the specification is satisfied. However, this is unsatisfactory for safety-critical systems, where the goal is to ensure that the system always satisfies the property. For example, space projects which have millions of components, where there is a combinatorial explosion of state space. This is where developing efficient techniques of verification becomes important.
For my PhD, I worked on timed automata, which is used to express settings with time constraints. My goal was to develop efficient algorithms to address networks of timed automata, which are commonly used to model complex real-time systems. A lot of the work in this area asks verification questions such as ‘Does this system satisfy a property?’. But one could also ask a complementary question ‘Can we automatically generate a system that meets a given logical specification?’. This is called synthesis, which is also something that I have been working on.
During my postdoc, I wanted to do more theory, and so I explored the extensions of automata models, where I looked into the inherent connections between machine models, logical formalisms, and algebraic structures, and developed procedures to transform one to the other, which is very important from an algorithmic context. During my second postdoc, my goal was to look at models of modern processors and programming languages. The question that interested me was, ‘Can you develop theoretical models for the behaviour of these processors and formally prove the correctness of these models?’. Additionally, I have also been interested in developing algorithmic techniques to say that a processor’s behaviour is ‘good’ in some sense. In ongoing work that I am quite excited about, there is a new framework that we are working on which brings together programming language models and some of the automata related techniques that I was looking at previously.
What are some of your other interests?
I enjoy reading books and watching movies. Also watching football; I used to play football earlier.
Back Subscribe
