Presented at the 35th International Conference on Computer Aided Verification, the honor recognizes significant contributions to the verification of concurrent programs through context-bounded analysis.
Recently, the Computer Sciences department’s Professor Tom Reps was awarded the prestigious 2023 CAV Award. Presented at the 35th International Conference on Computer Aided Verification (CAV), the distinction is awarded annually in honor of “fundamental contributions to the field of Computer-Aided Verification.”
As one of the foremost academic conferences in software engineering, CAV convenes leaders in academia, research, and industry to further the conceptual and real-life applications of computer-aided formal analysis. This branch of computer science develops tools to improve digital environments—such as those designed at Amazon, Facebook, Google, and Microsoft—through programmatic fact-checking that either proves a system’s correctness or discovers bugs that can lead to unexpected behavior, security vulnerabilities, crashes, or unresponsive software. Combining complex mathematical proofs and specially tailored algorithms, the goal is to improve the verification technologies available today.
Award-winning, game-changing research
The award’s co-recipients include Akash Lal (Microsoft Research), Madan Musuvathi (Microsoft Research), Jakob Rehof (TU Dortmund), and Shaz Qadeer (Meta Research), all distinguished alongside Reps “for the introduction of context-bounded analysis and its application to the systematic testing of concurrent programs.” Specifically, Reps is nominated for his research and findings in Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis (2009), co-written with Lal, who earned his Ph.D. from UW-Madison’s Computer Sciences department in 2009.
Originally appearing in Formal Methods in System Design, Reps’ and Lal’s paper built off the work posited by their co-recipients and demonstrated that context-bound analysis is able to verify programs as accurately as—and more efficiently than—a full verifier.
“After going down multiple blind alleys, we found a new trick, which Akash found an even simpler way to instantiate,” says Reps. “At Microsoft . . . Shaz, Akash and the other three honorees carried out additional research and built practical tools based, in part, on the ideas from the work at Wisconsin.”
Thanks to this collaboration, programmers have access to new tools to make their jobs easier. “The Microsoft tool Coyote, which incorporates ideas from the work honored by the CAV award, supports systematic exploration of the enormous number of behaviors that a concurrent program can have,” explains Reps. “It has a small barrier to entry, and users report previously unheard-of levels of test coverage. This helps programmers validate that their programs run as intended.”
A longstanding question with a “simple and powerful” answer
Praised by peers as an “elegant” idea with a tremendous impact on both the theory and practice of program verification, the awardees’ body of research succinctly answers a question that has been at the core of CAV since its inaugural conference in 1989: Can we devise effective techniques for checking the behaviors of a concurrent program in light of the state-space explosion problem (i.e., as the numbers of state variables increase, the number of reachable states grows exponentially)?
As their research proves, the answer is yes.
“This is a simple and powerful idea,” explained Parosh Abudullah, award committee chair and chaired professor at Uppsala University’s Department of Information Technology, while presenting the award in Paris. “It has led to new paradigms,” he adds—notably in sequentialization, weak memory models, and side-channel attacks— “which is really amazing.” For researchers in the field, it means brand new avenues to explore.
In short, the recognition “shows the caliber of students, such as Akash Lal, that the Computer Sciences department is able to attract,” Reps continues. Further, “it affirms the reputation of the madPL group—and the department more broadly—in the field of computer-aided verification.”
Reps isn’t the only one who thinks so. “The CAV Award recognizes the importance of Tom’s research in computer-aided verification. It affirms the high value that our Computer Sciences department has placed on his research over many years,” says Stephen Wright, chair of UW-Madison’s Computer Science Department. “This collaboration between Tom and Akash will have an enduring impact on program verification—and on software engineers and indeed all users of computer software.”
Reps is a leading model checking researcher and J. Barkley Rosser Professor & Rajiv and Ritu Batra Chair whose peer-reviewed publications have been cited more than 25,000 times. Since joining the UW-Madison faculty in 1985, he has been recognized as an ACM Fellow, Guggenheim Fellow, and Packard Fellow, in addition to being honored with the 2017 ACM SIGPLAN Programming Language Achievement Award. He is the second UW-Madison faculty member to be recognized by CAV, joining 2015 CAV Awardee Somesh Jha, Lubar Professor of Computer Sciences at UW-Madison.