Auditorium (ground floor)
14 February 2019 - 14h00
Concurrency bug detection at scale with Infer
by Nikos Gorogiannis from Facebook
Abstract: Concurrency bugs are notoriously difficult to reason about in program verification.
I will present two static analyses deployed at Facebook for detecting (a) data races and (b) deadlocks, both for Java code. These analyses have low-FP rates as a core design goal, and are implemented in the open-source Infer analyser. I will discuss the design trade-offs of these analyses, our experience from deploying them in production, as well as theoretical results on their completeness.