Every year, Microsoft’s research division awards two-year PhD fellowships to promising graduate students studying computer science, electrical engineering, mathematics, and related fields. To scope out these researchers, Microsoft undertakes an exhaustive process: first, department chairs from each university nominate up to nine of their best candidates. From there, each applicant is rigorously vetted, and finalists undergo an entire day of interviews with Microsoft researchers to determine the recipients. This year, Saswat Padhi, a third year Ph.D. student at the UCLA Computer Science Department, was named one of 10 recipients of this prestigious award, recognized for his accomplishments in practical software verification. The fellowship will cover Padhi’s tuition, housing, and conference and travel expenses, as well as offer him the opportunity to intern with a Microsoft researcher.
Padhi’s research goal is to provide practical solutions for developing reliable software. Today, advancements in software development allow for new programs to be churned out faster than ever before, but with the advancement of software comes the even faster growing problem of lurking bugs and security vulnerabilities. Padhi aims to prevent these issues by turning to a new way of building software that makes it easier for developers to guarantee that a program conforms to its desired behavior, while at the same time preventing bugs and security breaches before shipping the program to product.
Software verification asks the important question: Are we building the product right? Naturally, software verification is very difficult to accomplish because developers have to formally specify the desired behavior of their software and then prove that the software meets this specification, two tasks which are highly onerous and error-prone. Padhi hopes to simplify this process by developing solutions that allow users to interactively generate clearer, more dependable specifications for their software. He collects insights about program behavior – both from the program itself and the data generated during its execution – to propose possibly interesting properties to developers. From there, developers are able to improve on these suggestions and finalize them into specifications for their software, using Padhi’s tools to help verify their correctness. This approach has enormous implications for making software verification more accessible to developers and will hopefully revolutionize our ability to create reliable, bug-free software.
Padhi completed his undergraduate degree in Computer Science and Engineering at the Indian Institute of Technology, which was ranked as India’s top university in 2014. During his time as an undergrad, Padhi held multiple internships both in academia and industry. At his internship at TU Braunschweig in Germany, he explored databases and knowledge systems, and during his senior year he interned at Google, where he worked on high performance computing and Borg, Google’s cluster management system. He eventually found his true passion in research and joined the PhD program at UCLA after graduating from IIT Bombay in 2014. He is advised by Professor Todd Millstein, who specializes in programming languages. Padhi’s achievements are impressive, but not surprising, according to Millstein, as Padhi “naturally possesses the qualities of a good researcher, always asking the right questions, thinking about problems deeply, and pursuing topics which have a strong theoretical foundation but also are capable of being transformed into practical tools”.
Padhi says he will use the fellowship to continue his research on practical software verification, and hopes he will be able to provide an easier, more interactive method of verifying software. Last year, Padhi interned for the Microsoft PROSE group, where he worked on data-driven specification generation by “combining program synthesis and machine learning insights to cluster similar data based on patterns synthesized from data”. He will be returning to Microsoft this year to explore a related project on learning over semi-structured data, where he aims to learn complex patterns in spreadsheets and report inconsistencies using deep learning techniques.