Scaling Summary Computation of Large Java Libraries

We wish to pre-compute results of analyzing reachability of error conditions in large libraries. Our analysis uses exhaustive state-space exploration of an abstraction of the library code to discover all its possible behaviors, and represent them as method summaries. This exploration takes considerable time and space when analyzing large libraries. We present new techniques to speed up this exploration. Our techniques are based on empirical observations from trying to analyze large programs. Two of our techniques attempt to reduce the number of different environments under which a method must be explored, the first by identifying a dominant predicate that renders the other predicates immaterial to the outcome of a method, and the second by filtering out infeasible initial environments. A third technique re-uses the results of exploration of certain inner methods in a library by representing state information in a parameteric way. Together, these techniques enable us to compute reachability summaries of libraries with hundreds of methods.

By: Mangala Gowri Nanda; Satish Chandra

Published in: RC24271 in 2007


This Research Report is available. This report has been submitted for publication outside of IBM and will probably be copyrighted if accepted for publication. It has been issued as a Research Report for early dissemination of its contents. In view of the transfer of copyright to the outside publisher, its distribution outside of IBM prior to publication should be limited to peer communications and specific requests. After outside publication, requests should be filled only by reprints or legally obtained copies of the article (e.g., payment of royalties). I have read and understand this notice and am a member of the scientific community outside or inside of IBM seeking a single copy only.


Questions about this service can be mailed to .