For computer scientists who work on automated software verification and bug finding, CAV (the Computer-Aided Verification conference) is the premier annual scientific conference dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. I’m delighted to announce that Josh Berdine, Cristiano Calcagno, Dino Distefano, and Peter O’Hearn jointly with Samin Ishtiaq, the late John Reynolds, and Hongseok Yang, were honored with the 2016 CAV award. This award recognizes their contributions to the development of Separation Logic, the theory that underpins the Infer static analyzer.
CAV award winners Dino, Cristiano, Peter, and Josh.
Infer has been instrumental in bug detection at Facebook. Our engineers fix over 1,000 bugs every month that Infer detects in their diffs. And it’s relied upon by the engineering teams outside of Facebook as well, at companies like Spotify and Uber.
Infer uses Separation Logic, which is an extension of an earlier system called Hoare logic, to model the behavior of a program and allow reasoning about a program’s heap structures and pointer manipulation.
The heap is the key aspect of imperative programs that makes their verification difficult. Separation Logic provides the fundamental paradigm for compositional reasoning which allows modelling the heap to be both tractable and scalable. I can’t overstate its impact, since its introduction in 2000, on the world of automated verification. It was a true breakthrough that changed the community’s way of thinking, and opened the door to a wide field of research that lead to the development of efficient verification tools for heap manipulating programs.
After Peter introduced Separation Logic in his seminal 2000 paper, a team formed by Josh, Cristiano, Dino, Peter and Hongseok Yang took on the challenge of demonstrating it in practice. This led to over a decade of papers, proofs of concept, and breakthroughs that eventually led to Cristiano, Dino, and Peter founding Monoidics, which specialized in automatic formal verification and analysis of software. Meanwhile, Josh worked with Byron Cook at Microsoft Research where they developed a tool called SLAyer, and in due course Byron introduced me to the Monoidics team, which fortunately for us led to their decision to join Facebook.
On top of the profound theoretical and practical impact of Separation Logic, one of the most impressive aspects in this team’s work has been adapting Infer to make it successful for Facebook Engineering’s way of working.
Traditional static analysis tools either couldn’t handle code bases of our size and complexity at all, or would require days at a time to do so. On top of which if they produced results at all, it was typically in a huge report containing tens or hundreds of thousands of elements, with a high rate of false results.
The Infer team has elegantly handled all of these huge challenges. It scales to a large, real-world code base, and instead of running slowly over a whole program at a time, it can quickly and incrementally update a base analysis. The team adopted Infer to rapidly report bugs on in-progress diffs, which is the key time when a busy engineer is most likely to respond to a bug report. And they tuned its behavior to deliver an unprecedented low rate of false reports.
The team’s serious focus on the practical usability of static analysis tools is a model example for the CAV community to carry out its research, and delivers a strong foundation to build even better tooling for us all. In the meantime, hats off to Dino, Cristiano, Josh, and Peter – and to the entire Facebook Infer team in London!