IIT Bombay’s student, Vrunda Dave, was runner-up in the very prestigious Beth Outstanding Dissertation Prize (BODP) 2022 award
The E. W. Beth Dissertation Prize, named in honour of the Dutch mathematician Evert Willem Beth, is instituted by the Association for Logic, Language, and Information (FoLLI) each year, and recognizes outstanding Ph.D. theses in the fields of Logic, Language, and Information. Dissertations are evaluated based on their technical depth, strength, and originality. The shortlisted theses will be published by FoLLI. This is the first time a thesis from India has made it to the shortlist of the Beth Prize. The committee was particularly impressed by the breadth, technical depth, and novelty of the results in Vrunda’s thesis.
Earlier this year, Vrunda’s thesis won an honourable mention at the ACM India Doctoral Dissertation Award 2021.
Here we learn more about Vrunda’s journey into academic excellence.
Thank you. I did my schooling in my hometown, Nadiad, Gujarat. I graduated with a B. Tech in Computer Science and Engineering from Dharmsinh Desai University, Nadiad. I got placed in TCS during my undergrad and did my last semester training at TCS Research, Pune. I wanted to pursue the same project after graduation, so I joined TCS research as an employee after my convocation. During that time, some of my colleagues were visiting IIT Bombay for a Ph.D. entrance exam and they encouraged me to apply for the same (with the aim of visiting the campus). But that visit soon transformed into something much more significant as IITB became my second home when I joined the Ph.D. in Computer Science here.
I heard about this award from my supervisor, Prof S. Krishna. Each year, FoLLI releases the call for nominations for this prize. A doctoral student cannot nominate him/herself. My nomination was sent by my guide. Along with the thesis, I had to send a ten-page abstract, a letter of nomination from the supervisor, and two recommendation letters from experts in the thesis area.
My research is in Formal Methods which forms the very basis for Formal Verification. Formal verification is a mathematical method of checking if a design or implementation like a software program or a computer processor chip works as intended. It does so by algorithmically checking the equality of models of the design/implementation (e.g., a logic circuit can be modelled by a state transition system) and its specification (usually described in some mathematical logic). It is a very popular and active research topic and hardware companies like Intel, AMD, Nvidia, Apple, etc. utilise formal verification for their products, replacing the age-old method of testing. It is also getting traction in the software industry with companies like Amazon and Microsoft leading the way.
Sure. So, at the foundation of this area is the correspondence between mathematical models of computations and logical specifications. One important mathematical model is the string transducer which transforms input strings into output strings using state transitions and other rules. Any program can be viewed as a function transforming input to output, and for a sequential programme, the inputs and outputs can be modelled as strings. Thus, a transducer is a very powerful and general model.
In my thesis, I have tackled several problems involving the mathematical model of string transducers.
Our first contribution is in establishing the right models for the transformation of infinite strings as captured by first-order logic. Infinite strings are a natural model for input/output for real-time systems where we ideally do not want to consider termination. For example, an operating system conceptually could be running forever, or a pacemaker should keep operating without stopping. This work involved proving the equivalence of our proposed models and logical specifications of string transformations.
Next, we provided an equivalent formalism for transformations in terms of expressions. People using computers very likely have used regular expressions for pattern matching when searching for files or websites, etc. Our work finds similar expressions for functions over strings.
Theoretical CS research is often about finding well-behaved and interesting classes of objects. As part of our third contribution, we investigated string transformation functions that are continuous (like calculus) and established relevant properties and algorithms for the same.
Finally, we looked at solvers for string constraints. This is a very recent area of research gaining in popularity due to the success of SAT and SMT solvers. Here we have equations representing constraints and the variables can only take strings as values --- that is, the solutions to the constraints are strings. We extended the class of equations for which solutions can be derived algorithmically.
Essentially the world is moving towards formal verification, and it is in its infancy. My belief is it will soon become an integral part of software development (it already is for hardware). My research hopefully strengthens the basis for this to happen.
IITB helped me in every possible way. This success is as much mine as it is my guide’s - Prof. S Krishna. It is important to have a good mentor in your journey, and I was fortunate enough to have Prof. Krishna who was not just a constant inspiration, support, and guide to me, but also a cheerful friend. I grew as a researcher due to my discussions with all my collaborators which were possible because of my supervisor’s active research profile, and the challenging environment provided by IIT via its connections with other research institutes across India and the world. During the initial years of my Ph.D., I could explore various areas of computer science through courses, and this helped me tremendously in developing the mathematical maturity required for research. Finally, I would like to add that the natural surroundings, the opportunities for physical and mental improvement at IIT Bombay, and the company of like-minded friends and colleagues played a very important role in my success as well.
As I mentioned above, formal verification is gaining popularity in academia as well as industry. I plan to keep contributing to this domain as I am passionate about the theory as well as its possible applications. There is some gap between industry application and academic research in this area. So, there is a lot of scope to bridge this gap and create bug-free hardware/software using a formal verification system.
That was truly an enlightening and compelling conversation with Vrunda. She is already doing some extraordinary research in the field of formal verification, and we are sure there are many more accolades coming her way in the future. Congratulations to Vrunda on her award and we wish her the very best for the future!