Moving Fast with Software Verification
For organisations like Facebook, high quality software is important. However, the pace of change and increasing complexity of modern code makes it difficult to produce error-free software. Available tools are often lacking in helping programmers develop more reliable and secure applications.
Formal verification is a technique able to detect software errors statically, before a product is actually shipped. Although this aspect makes this technology very appealing in principle, in practice there have been many difficulties that have hindered the application of software verification in industrial environments. In particular, in an organisation like Facebook where the release cycle is fast compared to more traditional industries, the deployment of formal techniques is highly challenging.
This paper describes our experience in integrating a verification tool based on static analysis into the software development cycle at Facebook.
KeywordsCode Change Runtime Error Separation Logic Soundness Property High Quality Software
Unable to display preview. Download preview PDF.
- 1.Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: Proceedings of the 2006 EuroSys Conference, Leuven, Belgium, April 18-21, pp. 73–85 (2006)Google Scholar
- 6.Constine, J.: Facebook acquires assets of UK mobile bug-checking software developer Monoidics. http://techcrunch.com/2013/07/18/facebook-monoidics
- 10.O’Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001)Google Scholar
- 11.Reps, T.W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: Conference Record of POPL 1995: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, pp 49–61 (1995)Google Scholar