DASE: document-assisted symbolic execution for improving automated software testing

We propose and implement a new approach, Document-Assisted Symbolic Execution (DASE), to improve automated test generation and bug detection. DASE leverages natural language processing techniques and heuristics to analyze program documentation to extract input constraints automatically. DASE then uses the input constraints to guide symbolic execution to focus on inputs that are semantically more important. We evaluated DASE on 88 programs from 5 mature real-world software suites: Coreutils, findutils, grep, Binutils, and elftoolchain. DASE detected 12 previously unknown bugs that symbolic execution without input constraints failed to detect, 6 of which have already been confirmed by the developers. In addition, DASE increases line coverage, branch coverage, and call coverage by 14.2--120.3%, 2.3--167.7%, and 16.9--135.2% respectively, which are 6.0--21.1 percentage points (pp), 1.6--18.9 pp, and 2.8--20.1 pp increases. The accuracies of input constraint extraction are 97.8--100%.