PEQcheck: Localized and Context-aware Checking of Functional Equivalence (Technical Report)
Marie-Christine Jakobs

TL;DR
PEQcheck is a novel verification tool that efficiently checks the functional equivalence of refactored code segments by considering context and localization, improving accuracy and performance over prior methods.
Contribution
This paper introduces PEQcheck, a context-aware, localized equivalence checker that reduces verification tasks and enhances efficiency in ensuring refactoring correctness.
Findings
PEQcheck is sound and reliable.
Localized checking improves verification efficiency.
Context-awareness benefits equivalence accuracy.
Abstract
Refactorings must not alter the program's functionality. However, not all refactorings fulfill this requirement. Hence, one must explicitly check that a refactoring does not alter the functionality. Since one rarely has a formal specification of the program's behavior, we utilize the original program as functional specification. Then, we check whether the original and refactored program are functionally equivalent. To this end, we apply a common idea and reduce equivalence checking to program verification. To increase efficiency, our equivalence checker PEQcheck constructs one verification task per refactored code segment instead of one per function as typically done by prior work. In addition, PEQcheck considers the context of the code segments. For instance, only variables that are modified and live are required to be equivalent and read-only variables may be shared between original…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware Testing and Debugging Techniques · Software Engineering Research · Formal Methods in Verification
