kirancodes.me
To Proof Maintenance & Beyond!
FSE 2020

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

Vaibhav Sharma, Soha Hussein, Michael W. Whalen, Stephen McCamant, Willem Visser

PDFDOI 10.1145/3368089.3409734dblp

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.

BibTeX
@inproceedings{Sharma-al:FSE20,
  author    = {Vaibhav Sharma and
               Soha Hussein and
               Michael W. Whalen and
               Stephen McCamant and
               Willem Visser},
  title     = {Java Ranger: statically summarizing regions for efficient symbolic execution of Java},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {123--134},
  publisher = {{ACM}},
  year      = {2020},
}

Related papers