Java Ranger: Statically Summarizing Regions for Efficient Symbolic Execution of Java
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.
Fri 13 Nov Times are displayed in time zone: (UTC) Coordinated Universal Time change
| 01:00 - 01:02 Talk | ARDiff: Scaling Program Equivalence Checking via Iterative Abstraction and Refinement of Common Code Research Papers Sahar BadihiUniversity of British Columbia, Canada, Faridah AkinotchoUniversity of British Columbia, Canada, Yi LiNanyang Technological University, Singapore, Julia RubinUniversity of British Columbia, Canada DOI Pre-print | ||
| 01:03 - 01:04 Talk | Java Ranger: Statically Summarizing Regions for Efficient Symbolic Execution of Java Research Papers Vaibhav SharmaUniversity of Minnesota, USA, Soha HusseinUniversity of Minnesota, USA / Ain Shams University, Egypt, Michael WhalenUniversity of Minnesota, USA, Stephen McCamantUniversity of Minnesota, USA, Willem VisserStellenbosch University, South Africa DOI | ||
| 01:05 - 01:06 Talk | PCA: Memory Leak Detection using Partial Call-Path Analysis Tool Demos Wen Li, Haipeng CaiWashington State University, USA, Yulei SuiUniversity of Technology Sydney, David ManzPacific Northwest National Laboratory, USA DOI | ||
| 01:07 - 01:08 Talk | SWAN: A Static Analysis Framework for Swift Tool Demos Daniil TiganovUniversity of Alberta, Canada, Jeff ChoUniversity of Alberta, Karim AliUniversity of Alberta, Julian DolbyIBM Research, USA DOI | ||
| 01:09 - 01:10 Talk | UBITect: A Precise and Scalable Method to Detect Use-before-Initialization Bugs in Linux Kernel Research Papers Yizhuo ZhaiUniversity of California at Riverside, USA, Yu HaoUniversity of California at Riverside, USA, Hang ZhangUniversity of California at Riverside, USA, Daimeng WangUniversity of California at Riverside, USA, Chengyu SongUniversity of California at Riverside, USA, Zhiyun QianUniversity of California at Riverside, USA, Mohsen LesaniUniversity of California at Riverside, USA, Srikanth V. KrishnamurthyUniversity of California at Riverside, USA, Paul YuU.S. Army Research Laboratory, USA DOI | ||
| 01:11 - 01:30 Talk | Conversations on Static Analysis Paper Presentations Daniil TiganovUniversity of Alberta, Canada, Haipeng CaiWashington State University, USA, Sahar BadihiUniversity of British Columbia, Canada, Yizhuo ZhaiUniversity of California at Riverside, USA, M: Paul GazzilloUniversity of Central Florida | ||