Aldrich and Le Goues Tapped for Facebook Research Awards
Two ISR faculty members, Jonathan Aldrich and Claire Le Goues, were recently tapped as recipients of two Facebook Testing and Verification Research Awards.
The award by the tech giant aims to fund research that will lead to direct impact on the deployment and real world impact of Testing and Verification techniques in the technology sector.
In a video announcement calling for submissions, Peter O’Hearn (Research Scientist, Facebook Infrastructure) and Mark Harman (Engineering Manager, Facebook Infrastructure) noted that the award is not just a one-way tech transfer to industry, but something more reciprocal.
“Testing and verification research ideas are being deployed in major companies to help programmers do their jobs on a daily basis,” O’Hearn noted. “But, not only that, the act of deploying these ideas has caused us to find new scientific challenges that we haven’t thought of before.” Building on that, Harman explains, “When we first arrived at Facebook, I think both of us probably felt that, really, our job was about tech transfer. But, actually what surprised both of us is that we found that we were encountering new scientific challenges on an almost weekly basis.”
Aldrich’s proposal, “Incremental Verification, Gradually”, aims to address the monolithic nature of current verification technologies. It is often difficult to apply today’s tools to to verify partial properties, or to verify one component within a larger system. Inspired by gradual typing, Aldrich and his group are developing a system for gradual verification, allowing software engineers to specify and verify only the properties and components that are the most important--and allowing them to increase the scope of verification incrementally over time.
Le Goues’ submission, “Improving Analysis via Automated Program Transformation”, looks to grapple with the fact that, whether it is dynamic or static code analysis, automated analysis tools must approximate, both theoretically and in the interest of practicality. This approximation, Le Goues notes, can lead to disastrous misalignment between program reality (i.e., custom protocols or quality concerns) and tool assumptions. Le Goues and her group propose that techniques from their dynamic and static program repair research - notably automated transformation - can help improve the performance of automated bug-finding analyses.
For both researchers, the award means a great deal. “We are delighted to work with Facebook, which gives us an opportunity both to do fundamental research and to see new verification ideas having a transformative impact on industry” Aldrich notes. And Le Goues echoes this excitement to be working with practitioners to shape the future of verification. “Working with Facebook in particular is really exciting because they are developing cutting-edge tools for both automatic bug finding and, more recently, automatic bug fixing. We're excited to build on those advances,” she explains. “And we’re excited to partner more closely with the engineers and researchers within Facebook who have key perspective/experience on what they really need as well as the interest and ability to push novel tools and techniques to those in practice.”