Open Collections

Teixeira, Tarcisio

University of British Columbia

This thesis presents a novel technique for the comprehensive analysis and characterization of differences between two versions of a method. Building upon the foundations of Differential Symbolic Execution [13], our approach extends the concept of equivalence to effectively prove method functional equivalence or, when not equivalent, provide input constraints that narrow down the input space leading to divergent behaviors. To evaluate the effectiveness of our approach, we developed a prototype tool and conducted an extensive study using the IntroClass benchmark for Java. Our research sought to answer two critical research questions: 1) the effectiveness of our approach in classifying functionally equivalent programs compared to a standard partition-effects equivalence technique, and 2) the robustness of our approach in restricting the input space to pinpoint behavioral differences. The results of our evaluation demonstrate the significant potential of our approach in specifying the differences between method versions by characterizing the partition of the input space where those differences unfold. While our technique can establish program equivalence, we acknowledge that further evaluation and real-world application are needed to fully validate its practical competency. This thesis contributes a promising methodology for analyzing and characterizing method differences, offering a valuable tool for software engineers and researchers in the field of program analysis and verification. Future research and real-world applications could provide additional insights into the practical benefits and limitations of this approach.

Text

2023-09-28

Attribution-NonCommercial-NoDerivatives 4.0 International

http://hdl.handle.net/2429/86051

Computer Science

University of British Columbia

UBCV

http://creativecommons.org/licenses/by-nc-nd/4.0/