Adithya Murali comes to UW-Madison from University of Illinois-Urbana Champaign, where he completed his PhD on program verification and program synthesis. He says he is “deeply passionate about the fundamental aspects of problem solving and computational thinking, and looking at how to provide a structured playing field where humans and computers can perform computational tasks and come away with ironclad guarantees about the quality of the output.” He sums up why he came to UW in one word: “vibes.” Read more below!
Hometown: Chennai, India
Educational/professional background:
Bachelor’s degree in Mathematics and Computer Science at BITS Hyderabad, India (2017) followed by a PhD in Computer Science at UIUC (2024)
How did you get into your field of research?
For as long as I can remember, I have been enamoured with symbol manipulation and the idea that we could understand the nature of various structures by looking at the equations that they obeyed, an ‘algebra’. Along the way during my undergraduate education in mathematics, I was fortunate enough to have mentors who pointed out that computer science was rife with these structures and it was a much younger field than pure mathematics. I was motivated by the prospect of being an early contributor to a hugely important field. I have diversified my interests quite a bit since then, but the heart of my passion still lies in being able to glean structure in the world—and perhaps teaching computers to glean it for us!
What are your areas of focus?
I work in programming languages, specifically program verification and program synthesis. Logic and data-driven learning are predominant themes in most of my research.
What main issue do you address or problem do you seek to solve in your work?
The overarching focus of my research is to democratize software verification, enabling programmers who are not verification experts to verify their code. I’m intrigued by the idea of making verification technology broadly accessible by lowering the cognitive burden involved in automated software verification.
A primary focus of my work has been to develop data-driven logic learning techniques (learning logical formulas from data) to replace the expert help currently required in automated software verification. More generally, I also work in the area of program synthesis, and have a big interest in exploring questions at the intersection of verification/synthesis and machine learning.
We like to share the work of our faculty far and wide and make it accessible to all audiences. Please tell us about something you’re working on in layperson’s terms, so that non-computer scientists at UW-Madison and the general public can understand what you’re passionate about.
Software engineers and AI tools write mountains of code today from very high level requirements. One usually ensures the quality and reliability of this code using tests. This is only a guarantee insofar as you trust the person writing the tests to have left no stone unturned in poking the system for rough edges. But does this trust really hold up if the code is controlling a self-driving car careening towards you? There is a much higher standard that we can place on them in the form of a proof (like a math proof). It’s a 100% guarantee, but it’s also incredibly hard to achieve and can only be done with a large team of experts today. This is true even when the code is actually correct and the programmer can argue why it’s correct (to a human).
I’m interested in bridging this gap and trying to understand how explicating a mental model of correctness can be made into a routine aspect of software development. Beyond the obvious rhetoric of the comfort that absolute proof provides, I am deeply passionate about the fundamental aspects of problem solving and computational thinking, and looking at how to provide a structured playing field where humans and computers can perform computational tasks and come away with ironclad guarantees about the quality of the output. This applies to programming, writing mathematical proofs, legal reasoning, education, and a number of other application areas.
What’s one thing you hope students who take a class with you will come away with?
I hope that my classes can rewire their brains in a fundamental way and enable them to view the world in a richer, fuller way with new challenges that they can understand—and hopefully solve.
What attracted you to UW-Madison?
Vibes. But seriously, I came away from every conversation I had with my (now) colleagues feeling like I had a group of smart, enthusiastic friends that I could chat with about science and about life.
What was your first visit to campus like?
I drove into the city the day before my interview and took a stroll along Monona. I remember thinking what it would be like to make a home in a beautiful place like this.
What are you looking forward to doing or experiencing in Madison?
Learning a winter sport 🙂
Do you feel your work relates in any way to the Wisconsin Idea? If so, please describe how.
I absolutely believe that my passions have a place within the Wisconsin Idea. The reliability of digital automation isn’t just a technical idea, it’s a concept that touches upon the nature of how we perceive computers and what they can do for us as a society. Voting machines are a clear example of how trust (or lack thereof) in digital automation can have an outsized impact on society. I’m interested in working with both experts and non-experts to understand the kinds of guarantees they want about the code they write and use.
Hobbies/other interests:
I learned Indian classical music vocals for many years during my childhood. I’m still an avid listener and attend concerts. When I’m goofing off, I watch all kinds of fun movies (yes, including Christmas movies!)