Title
Enhancing symbolic execution with veritesting
Abstract
We present MergePoint, a new binary-only symbolic execution system for large-scale and fully unassisted testing of commodity off-the-shelf (COTS) software. MergePoint introduces veritesting, a new technique that employs static symbolic execution to amplify the effect of dynamic symbolic execution. Veritesting allows MergePoint to find twice as many bugs, explore orders of magnitude more paths, and achieve higher code coverage than previous dynamic symbolic execution systems. MergePoint is currently running daily on a 100 node cluster analyzing 33,248 Linux binaries; has generated more than 15 billion SMT queries, 200 million test cases, 2,347,420 crashes, and found 11,687 bugs in 4,379 distinct applications.
Year
DOI
Venue
2014
10.1145/2568225.2568293
Commun. ACM
Keywords
Field
DocType
symbolic execution,veritesting,verification,testing and debugging,semantics of programming languages
Code coverage,Programming language,Computer science,Parallel computing,Real-time computing,Software,Concolic testing,Symbolic execution,Test case,Symbolic trajectory evaluation
Conference
Volume
Issue
ISSN
59
6
0001-0782
Citations 
PageRank 
References 
66
1.88
33
Authors
4
Name
Order
Citations
PageRank
Thanassis Avgerinos186331.86
Alexandre Rebert22327.99
Sang Kil Cha354227.02
David Brumley42940142.75