Abstract
We present MergePoint, a new binary-only symbolic execution system for large-scale testing of commodity off-the-shelf(COTS) software. MergePoint introduces veritesting, a newtechnique that employs static symbolic execution to amplifythe effect of dynamic symbolic execution. Veritesting allowsMergePoint to find twice as many bugs, explore orders of magnitude more paths, and achieve higher code coverage thanprevious dynamic symbolic execution systems. MergePointis currently running daily on a 100 node cluster analyzing33,248 Linux binaries; has generated more than 15 billionSMT queries, 200 million test cases, 2,347,420 crashes, andfound 11,687 bugs in 4,379 distinct applications.
keywords: Veritesting, Symbolic Execution, Verification