Gao, Zheng;
(2022)
Facilitating Program Analysis through Transformation.
Doctoral thesis (Ph.D), UCL (University College London).
Preview |
Text
thesis.pdf - Other Download (1MB) | Preview |
Abstract
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.
| Type: | Thesis (Doctoral) |
|---|---|
| Qualification: | Ph.D |
| Title: | Facilitating Program Analysis through Transformation |
| Open access status: | An open access version is available from UCL Discovery |
| Language: | English |
| Additional information: | Copyright © The Author 2022. Original content in this thesis is licensed under the terms of the Creative Commons Attribution-NonCommercial 4.0 International (CC BY-NC 4.0) Licence (https://creativecommons.org/licenses/by-nc/4.0/). Any third-party copyright material present remains the property of its respective owner(s) and is licensed under its existing terms. Access may initially be restricted at the author’s request. |
| UCL classification: | UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science UCL > Provost and Vice Provost Offices > UCL BEAMS > Faculty of Engineering Science > Dept of Computer Science UCL > Provost and Vice Provost Offices > UCL BEAMS UCL |
| URI: | https://discovery-pp.ucl.ac.uk/id/eprint/10149388 |
Archive Staff Only
 |
View Item |
