Title
Dynamic symbolic execution for polymorphism.
Abstract
Symbolic execution is an important program analysis technique that provides auxiliary execution semantics to execute programs with symbolic rather than concrete values. There has been much recent interest in symbolic execution for automatic test case generation and security vulnerability detection, resulting in various tools being deployed in academia and industry. Nevertheless, (subtype or dynamic) polymorphism of object-oriented programs has been neglected: existing symbolic execution techniques can explore different targets of conditional branches but not different targets of method invocations. We address the problem of how this polymorphism can be expressed in a symbolic execution framework. We propose the notion of symbolic types, which make object types symbolic. With symbolic types,[ various targets of a method invocation can be explored systematically by mutating the type of the receiver object of the method during automatic test case generation. To the best of our knowledge, this is the first attempt to address polymorphism in symbolic execution. Mutation of method invocation targets is critical for effectively testing object-oriented programs, especially libraries. Our experimental results show that symbolic types are significantly more effective than existing symbolic execution techniques in achieving test coverage and finding bugs and security vulnerabilities in OpenJDK.
Year
DOI
Venue
2017
10.1145/3033019.3033029
CC
Keywords
Field
DocType
Concolic Testing, Object-Oriented Programs
Code coverage,Programming language,Vulnerability (computing),Object type,Computer science,Theoretical computer science,Concolic testing,Symbolic execution,Program analysis,Semantics,Vulnerability
Conference
Citations 
PageRank 
References 
4
0.40
46
Authors
3
Name
Order
Citations
PageRank
Lian Li118940.80
Yi Lu2473.48
Jingling Xue31627124.20