Facilitating Program Analysis through Transformation

Computer programs are reaching every corner of human lives, becoming ever more important. This, in turn, raises the cost of program malfunctions. Preventing or diagnosing these malfunctions requires extensive program analysis, but not every program is amenable to a specific analysis technique. For example, symbolic execution does not scale on programs involving floating point numbers or strings, due to the limitations of contemporary SMT solvers. This thesis attempts to advance the state of the art by utilising program transformation to facilitate analysis. To this end, it first establishes that program transformation is indeed invaluable when used to enable analysis. Specifically, it, departing from convention, views static typing as a form of program transformation and empirically quantifies the early detection of bugs static typing offers at the cost of type annotations. Then, it proposes TYPERITE, a tool that serves as an enabler to program analysis. TYPERITE allows developers to customise types via program transformation to detect domain-specific errors or permit analysis. Finally, this thesis presents VALUESCOPE, a dynamic program analysis that tracks a value of interest observed in an execution, like a NaN or a null, through its propagation chain back to its origin