Moving Fast with Software Verification

被引:183
作者
Calcagno, Cristiano [1 ]
Distefano, Dino [1 ]
Dubreil, Jeremy [1 ]
Gabi, Dominik [1 ]
Hooimeijer, Pieter [1 ]
Luca, Martino [1 ]
O'Hearn, Peter [1 ]
Papakonstantinou, Irene [1 ]
Purbrick, Jim [1 ]
Rodriguez, Dulma [1 ]
机构
[1] Facebook Inc, Cambridge, MA 02142 USA
来源
NASA FORMAL METHODS (NFM 2015) | 2015年 / 9058卷
关键词
D O I
10.1007/978-3-319-17524-9_1
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
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.
引用
收藏
页码:3 / 11
页数:9
相关论文
共 11 条
[1]  
Ball T., 2006, Operating Systems Review, V40, P73, DOI 10.1145/1218063.1217943
[2]  
Berdine J, 2006, LECT NOTES COMPUT SC, V4111, P115
[3]   A Few Billion Lines of Code Later Using Static Analysis to Find Bugs in the Real World [J].
Bessey, Al ;
Block, Ken ;
Chelf, Ben ;
Chou, Andy ;
Fulton, Bryan ;
Hallem, Seth ;
Henri-Gros, Charles ;
Kamsky, Asya ;
McPeak, Scott ;
Engler, Dawson .
COMMUNICATIONS OF THE ACM, 2010, 53 (02) :66-75
[4]   Compositional Shape Analysis by Means of Bi-Abduction [J].
Calcagno, Cristiano ;
Distefano, Dino ;
O'Hearn, Peter W. ;
Yang, Hongseok .
JOURNAL OF THE ACM, 2011, 58 (06)
[5]  
Calcagno C, 2011, LECT NOTES COMPUT SC, V6617, P459, DOI 10.1007/978-3-642-20398-5_33
[6]  
Constine J., Facebook acquires assets of uk mobile bugchecking software developer monoidics
[7]  
Cousot P, 2005, LECT NOTES COMPUT SC, V3444, P21
[8]  
Cousot P, 2013, LECT NOTES COMPUT SC, V7737, P128
[9]   Development and Deployment at Facebook [J].
Feitelson, Dror G. ;
Frachtenberg, Eitan ;
Beck, Kent L. .
IEEE INTERNET COMPUTING, 2013, 17 (04) :8-17
[10]  
O'Hearn P., 2001, Computer Science Logic. 15th International Workshop, CSL 2001 10th Annual Conference of the EACSL. Proceedings (Lecture Notes in Computer Science Vol.2142), P1