Java Ranger: statically summarizing regions for efficient symbolic execution of Java [conference paper]
Maroon and gold gears illustration

Conference

28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering - November 8, 2020

Authors

Vaibhav Sharma (Ph.D. student), Soha Hussein, Michael W Whalen (adjunct assistant professor), Stephen McCamant (associate professor), Willem Visser

Abstract

Merging execution paths is a powerful technique for reducing path explosion in symbolic execution. One approach, introduced and dubbed “veritesting” by Avgerinos et al., works by translating abounded control flow region into a single constraint. This approach is a convenient way to achieve path merging as a modification to a pre-existing single-path symbolic execution engine. Previous work evaluated this approach for symbolic execution of binary code, but different design considerations apply when building tools for other languages. In this paper, we extend the previous approach for symbolic execution of Java.

Link to full paper

Java Ranger: statically summarizing regions for efficient symbolic execution of Java

Keywords

software engineering

Share