Java Ranger: statically summarizing regions for efficient symbolic execution of Java
Vaibhav Sharma, Soha Hussein, Michael W. Whalen, Stephen McCamant, 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.
Topics & Concepts
Symbolic executionComputer scienceJavaProgramming languageConcolic testingPath (computing)Control flowCode (set theory)The SymbolicParallel computingTheoretical computer scienceSoftwarePsychologyPsychoanalysisSet (abstract data type)Software Testing and Debugging TechniquesSoftware Reliability and Analysis ResearchSoftware Engineering Research