IEEE International Working Conference on Source Code Analysis and Manipulation (SCAM)
This paper describes some of the challenges and opportunities when deploying static and dynamic analysis at scale, drawing on the authors’ experience with the Infer and Sapienz Technologies at Facebook, each of which started life as a research-led start-up that was subsequently deployed at scale, impacting billions of people worldwide.
International Conference on Very Large Data Bases (VLDB)
This paper describes an end-to-end streaming join service that addresses the challenges above through a streaming join operator that uses an adaptive stream synchronization algorithm that is able to handle the different distributions we observe in real-world streams regarding their event times.
By: Gabriela Jacques da Silva, Ran Lei, Luwei Cheng, Guoqiang Jerry Chen, Kuen Ching, Tanji Hu, Yuan Mei, Kevin Wilfong, Rithin Shetty, Serhat Yilmaz, Anirban Banerjee, Benjamin Heintz, Shridhar Iyer, Anshul Jaiswal
This paper describes the end-to-end regression detection system designed and used at Facebook. The main detection algorithm is based on sequential statistics supplemented by signal processing transformations, and the performance of the algorithm was assessed with a mixture of online and offline tests across different use cases.
This paper describes work in continuous reasoning, where formal reasoning about a (changing) codebase is done in a fashion which mirrors the iterative, continuous model of software development that is increasingly practiced in industry. We suggest that advances in continuous reasoning will allow formal reasoning to scale to more programs, and more programmers.
This paper tells the story of the development of RacerD, a static program analysis for detecting data races that is in production at Facebook. The technical details of RacerD are described in a separate paper; we concentrate here on how the project unfolded from a human point of view.
16th International Conference on Software Engineering and Formal Methods
This paper briefly reviews Testability Transformation, its formal definition, and the open problem of constructing a set of formal test adequacy semantics to underpin the current practice of deploying transformations to help testing and verification activities.