Jaco Geldenhuys, a principal applied scientist with Amazon Web Services (AWS), and Willem Visser, an AWS senior principal applied scientist, won the 2022 International Symposium on Software Testing and Analysis (ISSTA) Impact Paper Award for their development of the concept of probabilistic symbolic execution, a novel method for deriving probabilities for the execution of computer code.
Their 2012 paper, “Probabilistic Symbolic Execution: Quantitative Program Analysis through Model Counting,” was coauthored with Matthew Dwyer, the Robert Thomson Distinguished Professor of Computer Science at the University of Virginia. It demonstrates how model counting estimates the probability of executing portions of a program rather than evaluating whether a constraint is true or false.
“This introduced a whole new field,” said Visser. “Nobody had done this before we did it. Typically, if there’s any issue in your code, that’s bad. You want to fix it. Now you can calculate the reliability of your program — because as long as ‘that thing’ doesn’t happen, your code will be fine, and you now know how likely it is to happen.”
A forum presented by the Association for Computing Machinery’s Special Interest Group on Software Engineering (ACM SIGSOFT), the ACM SIGSOFT ISSTA has been a leading research conference in software testing and analysis for 31 years. It awards the Impact Paper Award yearly to a 10-year-old paper that has significantly influenced research or the practice of software testing and analysis.
The paper by Geldenhuys, Visser, and Dwyer has had an impact on a number of applications involved with the methodical analysis of computer programs, especially those involving side channels in security applications. Side channels leak indirect information about a program’s operation — such as execution time — that attackers can exploit without having direct access to the code.
“There’s very little work in this specific application in this field that does not either directly or indirectly come from the paper,” Geldenhuys said. “For now, at least, our paper is still that root that the other work is growing out of. So that’s something that’s gratifying.”
The researchers noted their paper initially met with skepticism due to the complexity of the approach it described, which made the analysis expensive in terms of compute resources. The trio then collaborated on a second paper on how to make probabilistic analysis more efficient, publishing “Green: Reducing, Reusing and Recycling Constraints in Program Analysis” four months later.
“The work on reusing constraints ended up being generally applicable,” said Geldenhuys. “While we began the work to scale the probabilistic analysis, but, the same ideas worked wonders on different kinds of symbolic execution. That work took on a life of its own.”
South African citizens Geldenhuys and Visser met at Stellenbosch University when they studied under the same supervisor for their master’s degrees in computer science. Geldenhuys went on to earn his doctor of technology at Tampere University of Technology in Finland in 2005. He returned to Stellenbosch and worked as a professor until 2020, when he joined Amazon full time.
Visser earned his PhD in computer science from the University of Manchester in the United Kingdom in 1998. After working for the NASA Ames Research Center in Silicon Valley for 10 years, Visser returned to Stellenbosch to teach and reunited with Geldenhuys.
Dwyer met Geldenhuys and Visser in 2011, when he was awarded a Fulbright Scholar grant to perform research at Stellenbosch. As he worked alongside Geldenhuys and Visser in the application of symbolic execution tools over distribution problems, they stumbled upon the inspiration for the 2012 paper.
“It dawned on us that programs even without any random statements in them or anything that implies distribution are probabilistic anyway,” said Visser. “If some value should be equal to 42, for example, there is a very small likelihood that the input will actually be 42, that that specific execution will happen. So we started to think along the lines of, ‘Can we actually analyze a program in terms of how likely the executions are in the code?’ And that was ultimately the nugget that became this paper.”
Visser joined Amazon full time in November 2019 after just over a year as an Amazon consultant. Visser primarily works on Amazon CodeGuru, a developer tool that provides intelligent recommendations to improve code quality and identify an application’s most expensive lines of code.
Geldenhuys works in Amazon’s Automated Reasoning Group in AWS Identity and Access Management, where he develops tools and techniques to prove the correctness and security of permissions management systems used by all AWS customers.
“It’s a really fun challenge,” Geldenhuys said. “There are millions of customers who depend on the system. I enjoy working on problems where I can make life better for customers using my skill set.”
