The Association for Computing Machinery has named Ranjit Jhala, an Amazon Scholar and professor of computer science engineering at the University of California, San Diego, as a 2021 ACM Fellow for his “contributions to software verification.”
Software verification uses automated mathematical tools to check computer code, comparing it against a set of predetermined rules to isolate errors that can be frustrating, costly, and vulnerable to cyberattack. By automating software verification tools and creating a way for human programmers and computer algorithms to work side by side in real time, Jhala’s work has changed the paradigm in computer programming and earned him the designation as an ACM Fellow.
“There are only so many things that you can test,” Jhala said. “With these algorithms, what we try to do is find ways where, in addition to the code, the programmer can describe what they think the code should be doing in the first place. These kinds of tools work alongside them as they write the code, to make sure the spec matches what they’re actually building.”
Occasionally, when a program runs outside its normal operating parameters, small errors in code can cause applications to run improperly. Engineers call the resulting malfunctions corner cases. Corner cases can cause computer systems to crash or applications not to work properly. Over the last few decades, hackers have figured out how to exploit corner cases to infiltrate computer systems, injecting malware or stealing sensitive information from users.
Jhala’s work makes it easier for programmers to identify and fix corner cases before they present vulnerabilities to a system. A paper he coauthored in 2002, “Lazy Abstraction,” introduced the Berkeley Lazy Abstraction Software verification Tool (BLAST) and has become the most-cited paper of the past 20 years from the Principles of Programming Languages (POPL) symposium, a prestigious academic conference in computer science. Jhala’s work on the BLAST model checker underpins the design of many modern-day algorithms and remains a staple of many graduate-level computer programming classes.
Jhala also is a pioneer in the development of Liquid Types, a tool that facilitates collaboration between a programmer and automated deduction tools that help identify errors in code. “It’s much more of a tightly knit back-and-forth between the programmer and this tool as they’re developing,” Jhala said. “The programmer is more easily able to say what they want their code to do, and the system itself is able to quickly tell them, ‘Hey, I think there’s something wrong over here,’ while their program is in real time.”
Jhala received a bachelor of technology degree in computer science from the Indian Institute of Technology in Delhi. In 2004, he earned his PhD in electrical engineering and computer science from the University of California, Berkeley. He began working for Amazon in July 2019, when a colleague encouraged him to join Amazon’s Automated Reasoning Group.
As part of the ARG, Jhala has worked on practical applications of identity and access management, writing algorithms that help explain access control policies to users. He also works in Amazon’s CodeGuru Group, developing mathematical tools that look at programming code to determine if the code fits within a set of predetermined rules. “If I’ve done my job right, the end user shouldn’t see anything bad,” Jhala said.
With nearly 100,000 student and professional members, ACM is the leading professional society for academic computer scientists. The ACM Fellows program recognizes the top 1 percent of ACM members for their accomplishments in computing and information technology. ACM Fellows are nominated by their peers, and a distinguished selection committee chooses the awardees, who have contributed to the computing field in cloud database systems, deep learning acceleration, high-performance computing, robotics, theoretical computer science, and other specialties.
“Computing professionals have brought about leapfrog advances in how we live, work, and play,” said Gabriele Kotsis, ACM president. “The ACM Fellows program honors the creativity and hard work of ACM members whose specific accomplishments make broader advances possible.”
