Breakthroughs in Automated Formal Reasoning Lead to Gagandeep Singh's Prestigious Dissertation Award

Now in his first year as a faculty member at Illinois CS, Gagandeep Singh can easily recall the work that went into recently earning the John C. Reynolds Doctoral Dissertation Award –  the most, prestigious award a doctoral student in his research focus can win.

While studying at ETH Zurich, Singh poured his passion for research into a focus on formal methods, programming languages and artificial intelligence. Learning under professors Martin Vechev and Markus Püschel, who served as his co-advisers, Singh worked on creating new general algorithms to enable precise automated analysis of both numerical software and deep learning.

He stayed up countless nights discussing possibilities with his advisers. He ran into roadblocks. There were times he felt the breakthrough might not occur.

“But one night, you get an idea, and it all begins to fall into place. All of a sudden you’re on the verge of solving what you felt like was unsolvable,” Singh said. “I cannot exactly explain what that feeling is like, but no other feeling can compare. That’s what we researchers live for. Yes, it’s exhilarating, but that feeling also speaks to the hard work involved.”

Through his dedicated effort, Singh’s resulting dissertation – titled, “Scalable Automated Reasoning for Programs and Deep Learning” – earned the John C. Reynolds Award from ACM SIGPLAN.

Beyond the prestigious award and publication, Singh also desired something more. A major emphasis in his research is to also deliver accessible and installable systems that people in industry and academia use consistently.

The fact that he can now pursue those interests at Illinois CS, while recruiting and forming relationships with similarly driven students, is the beginning of his aspirations coming true.

“I am, of course, delighted to receive the John C. Reynolds Award, as it is something that I never planned for or even expected,” Singh said. “But the fact that I won it only further motivates me to continue pursuing all of my goals. I’m excited to go on similar journeys again, but this time with my students rather than as a pupil.”

Those students will undoubtedly grow from his approach to research and instruction.

Singh credits his advisers, Vechev and Püschel, with helping him learn his own strengths while providing the type of expertise he could rely on – a process he hopes to impart on his own students over time.

During their years together, Vechev provided insight into programing languages and formal methods while Püschel advised about high performance algorithm design.

The first few years, Singh said, his advisers encouraged him to focus on the tech itself and not to worry about the papers. Time spent doing this is how he developed a new method to online decomposition of program variables, which speeds up the Polyhedra domain considered to be impractical for over 40 years. Then, to address the analysis of deep learning models, his work provided a set of abstract domains, specifically designed for deep learning models, achieving the state-of-the-art results.

These advancements, once finalized, turned into two systems, ELINA and ERAN, which are available publicly online and include code that’s used by people in both academia and industry.

“The opportunity to learn from two people who are experts in their field turned into an amazing experience,” Singh said. “They also allowed me the freedom to grow, and I learned how to turn great advice into results. When you wish to become a faculty member yourself, you must grow beyond a reliance on your instructor.

“I look forward now to moments when the students I work with prove their own high level of comprehension and ability.”