Enhancing Symbolic Execution with Veritesting

被引：14
作者：
Avgerinos, Thanassis [1 ,2 ]
Rebert, Alexandre [1 ,2 ]
Cha, Sang Kil [2 ]
Brumley, David [1 ,2 ]
机构：
[1] AllSecure Inc, Pittsburgh, PA 15213 USA
[2] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA
来源：
COMMUNICATIONS OF THE ACM | 2016年 / 59卷 / 06期
关键词：
Model checking - Program translators - Software testing;
D O I：
10.1145/2927924
中图分类号：
TP3 [计算技术、计算机技术];
学科分类号：
0812 ;
摘要：
Symbolic execution is a popular automatic approach for testing software and finding bugs. Microsoft's symbolic executor SAGE is responsible for finding one-third of all bugs discovered during the development of Windows 7. Symbolic execution works by automatically translating program fragments to logical formulas. The logical formulas are satisfied by inputs that have a desired property. Researchers propose a new technique for symbolic execution called veritesting to enhance symbolic execution.
引用
收藏
页码：93 / 100
页数：8
相关论文
共 22 条
[1]  
Allen J.R., 1983, Proc. of the Symposium on Principles of Programming Languages. POPL, P177
[2]   Enhancing Symbolic Execution with Veritesting [J].
Avgerinos, Thanassis ;
Rebert, Alexandre ;
Cha, Sang Kil ;
Brumley, David .
36TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE 2014), 2014, :1083-1094
[3]  
Babic D, 2008, ICSE'08 PROCEEDINGS OF THE THIRTIETH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, P211, DOI 10.1145/1368088.1368118
[4]  
Bounimova E, 2013, PROCEEDINGS OF THE 35TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE 2013), P122, DOI 10.1109/ICSE.2013.6606558
[5]  
Cadar C., 2008, Proceedings of the 8th USENIX conference on Operating systems design and implementation, OSDI'08, (USA), P209
[6]   Symbolic Execution for Software Testing: Three Decades Later [J].
Cadar, Cristian ;
Sen, Koushik .
COMMUNICATIONS OF THE ACM, 2013, 56 (02) :82-90
[7]   Unleashing MAYHEM on Binary Code [J].
Cha, Sang Kil ;
Avgerinos, Thanassis ;
Rebert, Alexandre ;
Brumley, David .
2012 IEEE SYMPOSIUM ON SECURITY AND PRIVACY (SP), 2012, :380-394
[8]  
Chipounov V, 2011, ACM SIGPLAN NOTICES, V46, P265, DOI [10.1145/1961296.1950396, 10.1145/1961295.1950396]
[9]   Satisfiability Modulo Theories: Introduction and Applications [J].
De Moura, Leonardo ;
Bjorner, Nikolaj .
COMMUNICATIONS OF THE ACM, 2011, 54 (09) :69-77
[10]   Avoiding exponential explosion: Generating compact verification conditions [J].
Flanagan, C ;
Saxe, JB .
ACM SIGPLAN NOTICES, 2001, 36 (03) :193-205
123