Silencing the ‘Ticking Risk’ of System Failures

By Doug Hulette

For Aarti Gupta, failure is not an option. 

The computer science professor aims to develop techniques and methodologies to ensure that complex computer systems not only do what they’re designed to do but do it correctly every time. To eliminate what she calls the “ticking risk” of failures due to design bugs in increasingly complex hardware and software systems, her work focuses on formal verification of systems, program analysis, and automatic decision procedures for logics. 

“As we continue to reap the benefits of computing, it is imperative that we build mechanisms for checking these systems for correctness and avoiding failures,” Gupta says. “Such failures can be minor, as when our computer freezes on us; large-scale, as when airline systems break down; and sometimes lethal, as we saw recently in accidents with self-driving cars.”

“The most widely prevalent approach to avoiding failures is to test these systems using scenarios likely to be seen in practice. This is useful but leaves unanswered the question as to what happens in other scenarios. A more ambitious goal is to show that these systems always work as intended, or, equivalently, guarantee that you will find any deviations from intended behavior before these systems are deployed.”

Gupta recently earned special recognition for her work when the Association for Computing Machinery, considered the world's preeminent computing society, named her one of 54 new fellows, the group’s highest membership grade. She was cited for her “contributions to system analysis and verification techniques and their transfer to industrial practice.” 

“We have seen significant success in the development of analysis and verification methods that work in practice for large-scale systems, including hardware and software,” she says. “These methods essentially build a mathematical proof to show that the design will work as intended or in the process of trying to build the proof, find where the design will fail. These proofs are large and complicated, and finding ways of doing this automatically and efficiently present challenges that have driven my research.”

Before joining the CS faculty in 2015 as a full professor, Gupta led research in system analysis and verification at NEC Labs America, where she made contributions to algorithmic foundations and practical applications of hardware and software verification. She earned her Ph.D. in computer science from Carnegie Mellon University and a bachelor of technology degree in electrical engineering from the Indian Institute of Technology (Delhi, India).
 

In an email exchange, Gupta offered additional thoughts on her work and its importance:

When did you become interested in the challenges of working at the intersection of computer science and industry?

Research in computer science has always seen close interaction between research and industrial practice. Industry is constantly trying to innovate and provide new products and capabilities. Research provides new ideas that open up new possibilities, or clears fundamental roadblocks that are encountered on way to providing new capabilities. I have been fortunate to be part of this virtuous cycle where research enables industry through fundamental innovations, and industry drives research through providing opportunities and challenges. I was exposed to this during graduate school, and transitioned to the industry at NEC Labs following my Ph.D. NEC Labs provided an excellent environment where I could be at the frontier of research with wonderful collaborators, while at the same time engage with product teams to take the research ideas to industrial practice benefiting products widely used in society.

In what form have your contributions been transferred to industry practice?

My initial research at NEC Labs addressed hardware verification — ensuring that complex hardware systems worked correctly. This work was used in NEC electronic design automation products, as well as licensed to external companies that commercialized the research through their own products. As NEC moved away from hardware systems, the focus of my research shifted to software verification. Here I led a group that was successful in making several foundational contributions that we were able to combine in a software verification platform called Varvel. This has been deployed at NEC since 2010 and has been successfully applied on more than a hundred software projects, some with millions of lines of code. Also while at NEC, we openly published our research, enabling these ideas to influence other efforts.

How does your work affect the lives of everyday citizens?

Software and computing systems touch everyone’s lives — from apps on our phones to ever-increasing automation as seen in emerging driverless cars. Our research is working on making these systems more reliable, through efficient and effective techniques – and thus letting us build better and safer systems that can improve our lives in as yet unimaginable ways.

Why did you make the move from industry to education?

While at NEC Labs I had the opportunity to work with graduate students through their internships with my group. It was very exciting to see them eager to push the research frontier with their new ideas and mentor them through the process. With my move to academia, I can do this in a more complete way, and not just with Ph.D. students but also with undergraduates. I have enjoyed teaching sophomores in introductory courses, and several of them have been piqued by my research interests to take my graduate course on research techniques in software verification.

I am delighted to see many women in my graduate class, and hope that they will continue in research careers – we definitely need to increase the participation of women in research in computer science!