Scaling Java Program Analysis and Testing Techniques

Abstract

We are witnessing a significant surge in the development of large-scale software solutions, largely propelled by the extensive reuse of components and third-party libraries. Simultaneously, our reliance on software is intensifying, prompting an increasing demand for robust methods to validate and verify software behavior. Nevertheless, our current verification and testing methodologies frequently fall short when applied to these expansive systems. In the pursuit of addressing the challenges of constructing, validating, and testing large-scale software programs, this dissertation proposes enhancements to existing state-of-the-art tools and techniques, with the goal of improving their scalability. This dissertation presents three contributions: First, we present a novel algorithm that discovers integration problems of reused software components that arise from expecting the wrong contract for the component. Given an implemented software component, our algorithm checks if our assumed contract of the component's behavior is correct, i.e., matches the implementation. If a discrepancy is identified, our algorithm attempts to repair the hypothetical contract to a matching contract that satisfies the component's implementation. Second, we improve the scalability of Java program analysis by introducing path-merging to symbolic execution. Using this technique, instead of exploring all feasible paths one at a time, symbolic execution can collapse code regions into a disjunctive logical constraint, thereby reducing the number of execution paths that need to be executed. Finally, we improve the scalability of Java testing techniques by introducing type-based targeted mutation for generator-based fuzzers. This enhancement enables the fuzzer to generate effective inputs, accelerating the likelihood of achieving desired coverage targets.