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

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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. Because Java code typically contains many small dynamically dispatched methods, it is important to include them in multi-path regions; we introduce dynamic inlining of method-regions to do so modularly. Java's typed memory structure is very different from the binary representation, but we show how the idea of static single assignment (SSA) form can be applied to object references to statically account for aliasing. We have implemented our algorithms in Java Ranger, an extension to the widely used Symbolic Pathfinder tool. In a set of nine benchmarks, Java Ranger reduces the running time and number of execution paths by a total of 38% and 71% respectively as compared to SPF. Our results are a significant improvement over the performance of JBMC, a recently released verification tool for Java bytecode. We also participated in a static verification competition at a top theory conference where other participants included state-of-the-art Java verifiers. JR won first place in the competition's Java verification track.

Original languageEnglish (US)
Title of host publicationESEC/FSE 2020 - Proceedings of the 28th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering
EditorsPrem Devanbu, Myra Cohen, Thomas Zimmermann
PublisherAssociation for Computing Machinery, Inc
Pages123-134
Number of pages12
ISBN (Electronic)9781450370431
DOIs
StatePublished - Nov 8 2020
Event28th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2020 - Virtual, Online, United States
Duration: Nov 8 2020Nov 13 2020

Publication series

NameESEC/FSE 2020 - Proceedings of the 28th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering

Conference

Conference28th ACM Joint Meeting European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2020
Country/TerritoryUnited States
CityVirtual, Online
Period11/8/2011/13/20

Bibliographical note

Funding Information:
The research described in this paper has been supported in part by the Google Summer of Code program and by the National Science Foundation under grant 1563920.

Publisher Copyright:
© 2020 ACM.

Keywords

  • Path-merging
  • Symbolic execution
  • Veritesting

Fingerprint

Dive into the research topics of 'Java Ranger: Statically summarizing regions for efficient symbolic execution of Java'. Together they form a unique fingerprint.

Cite this