gether with crafted abstract domains
can scale: each procedure only needs
to be visited a few times, and many of
the procedures in a codebase can be
analyzed independently, thus opening opportunities for parallelism. A
compositional analysis can even have
a runtime that is (modulo mutual recursion) a linear combination of the
times to analyze the individual procedures. For this to be effective, a suitable abstract domain, for instance
limiting or avoiding disjunctions,
should also contain the cost of analyzing a single procedure.
Finally, compositional analyses are
naturally incremental—changing one
procedure does not necessitate re-ana-lyzing all other procedures. This is important for fast diff-time analysis.
This article described how we, as static
analysis people working at Facebook,
have developed program analyses in response to the needs that arise from production code and engineers’ requests.
Facebook has enough important code
and problems that it is worthwhile to
have embedded teams of analysis experts, and we have seen (for example, in
the use of Infer to support multithreaded Android News Feed, and in the evolution of Zoncolan to detect SEV-worthy
issues) how this can impact the company. Although our primary responsibility is to serve the company, we believe
that our experiences and techniques
can be generalize beyond the specific
industrial context. For example, Infer is used at other companies such as
Amazon, Mozilla, and Spotify; we have
produced new scientific results, 2, 10 and
proposed new scientific problems. 11, 14
Indeed, our impression as (former) researchers working in an engineering
organization is that having science and
engineering playing off one another in
a tight feedback loop is possible, even
advantageous, when practicing static
analysis in industry.
To industry professionals we say:
advanced static analyses, like those
found in the research literature, can be
deployed at scale and deliver value for
general code. And to academics we say:
from an industrial point of view the subject appears to have many unexplored
avenues, and this provides research opportunities to inform future tools.
Special thanks to Ibrahim Mohamed
for being a tireless advocate for Zoncolan among security engineers, to Cris-tiano Calcagno for leading Infer’s technical development for several years,
and to our many teammates and other
collaborators at Facebook for their
contributions to our collective work on
scaling static analysis.
Readers interested in more technical details of this work
are encouraged to review the online appendix; (https://
1. Bessey, A. et al. A few billion lines of code later: using
static analysis to find bugs in the real world. Commun.
ACM 53, 2 (Feb. 2010), 66–75.
2. Blackshear, S., Gorogiannis, N., Sergey, I. and O’Hearn,
P. Racerd: Compositional static race detection. In
Proceedings of OOPSLA, 2018.
3. Brookes, S. and O’Hearn, P. W. Concurrent separation
logic. SIGLOG News 3, 3 (2016), 47–65.
4. Calcagno, C. et al. Moving fast with software
verification. In Proceedings of NASA Formal Methods
Symposium, 2015, 3–11.
5. Calcagno, C., Distefano, D. O’Hearn, P. W and Yang,
H. Compositional shape analysis by means of bi-abduction. J. ACM 58, 6 (2011), 26.
6. Cook, B. Formal reasoning about the security of
Amazon Web services. LICS (2018), 38–47.
7. Cousot, P. and Cousot, R. Abstract interpretation: A
unified lattice model for static analysis of programs
by construction or approximation of fixpoints. In
Proceedings of the 4th POPL, 1977, 238–252.
8. Cousot, P. and Cousot, R. Modular static program
analysis. In Proceedings of 2002 CC, 159–178.
9. Feitelson, D.G., Frachtenberg, E. and Beck, K.L.
Development and deployment at Facebook. IEEE
Internet Computing 17, 4 (2013), 8–17.
10. Gorogiannis, N., Sergey, I. and O’Hearn, P. A true
positives theorem for a static race detector. In
Proceedings of the 2019 POPL.
11. Harman, M. and O’Hearn, P. From start-ups to scale-ups: Open problems and challenges in static and
dynamic program analysis for testing and verification).
In Proceedings of SCAM, 2018.
12. Iqbal, S. T and Horvitz, E. Disruption and recovery of
computing tasks: Field study, analysis, and directions.
In Proceedings of 2007 CHI, 677–686.
13. Larus, J.R. et al. Righting software. IEEE Software 21,
3 (2004), 92–100.
14. O’Hearn, P. Continuous reasoning: Scaling the impact
of formal methods. LICS, 2018.
15. O’Hearn, P. W. Experience developing and deploying
concurrency analysis at Facebook. SAS, 2018, 56–70.
16. O’Hearn, P. W. Separation logic. Comm. ACM 62, 2 (Feb
17. Sadowski, C., Aftandilian, E., Eagle, A., Miller-Cushon,
L. and Jaspan, C. Lessons from building static analysis
tools at Google. Commun. ACM 61, 4 (Apr. 2018), 58–66.
18. Xie, Y. and Aiken, A. Static detection of security
vulnerabilities in scripting languages. In Proceedings
of USENIX Security Symposium, 2006.
19. Yorsh, G., Yahav, E. and Chandra, S. Generating precise
and concise procedure summaries. In Proceedings of
Dino Distefano is a research scientist at Facebook,
London, U.K., and a professor of computer science at
Queen Mary University of London, U.K.
Manuel Fähndrich is a software engineer at Facebook
Research, Seattle, WA, USA.
Francesco Logozzo is a software engineer at Facebook
Research, Seattle, WA, USA.
Peter W. O’Hearn is a research scientist at Facebook,
London, U.K. and a professor of computer science at
University College London, U.K.
Copyright held by authors/owners.
tool failed to report them. To date, we
have had about 11 missed bugs, some
of them caused by a bug in the tool or
Compositionality and Abstraction
The technical features that underpin our analyses are
compositionality and abstraction.
The notion of compositionality comes
from language semantics: A semantics is
compositional if the meaning of a com-
pound phrase is defined in terms of the
meanings of its parts and a means of
combining them. The same idea can be
applied to program analysis. 5, 8 A program
analysis is compositional if the analysis
result of a composite program is defined
in terms of the analysis results of its parts
and a means of combining them. When
applying compositionality in program
analysis, there are two key questions:
For (a) we need to approximate the
meaning of a component by abstracting
away the full behavior of the procedure
and to focusing only on the properties
relevant for the analysis. For instance, for
security analysis, one may be only inter-
ested that a function returns a user-con-
trolled value, when the input argument
contains a user-controlled string, dis-
carding the effective value of the string.
More formally, the designer of the static
analysis defines an appropriate math-
ematical structure, called the abstract
domain, 7 which allows us to approxi-
mate this large function space much
more succinctly. The design of a static
analysis relies on abstract domains pre-
cise enough to capture the properties of
interest and coarse enough to make the
problem computationally tractable. The
‘abstraction of a procedure meaning’ is
often called a procedure summary in the
analysis literature. 19
The answer to question (b) mostly
depends on the specific abstract domain chosen for the representation of
summaries. Further information on
the abstractions supported by Infer
and Zoncolan, as well as brief information on recursion, fixpoints, and
analysis algorithms, may be found in
the online technical appendix. It is
worth discussing the intuitive reason
for why compositional analysis to-