Write a Blog >>
FormaliSE 2021
Tue 18 - Fri 21 May 2021
co-located with ICSE 2021
Wed 19 May 2021 15:30 - 16:00 at FormaliSE Room - Program verification

A refactoring must preserve the program’s functionality. However, not all refactorings are correct. Thus, preservation of the functionality must be checked. Since programs are rarely formally specified, we use the original program as functional specification and check whether the original and refactored program are functionally equivalent. More concretely, our PEQcheck technique follows a common approach and reduces equivalence checking to program verification. To increase efficiency, PEQcheck generates several verification tasks, namely one per refactored code segment and not one per function as typically done by prior work. Additionally, PEQcheck takes the context of the code segments into account. For example, only modified, live variables need to be equivalent and read-only variables can be shared between original and refactored code segments. We proved soundness of our PEQcheck technique and implemented it in a prototype tool. Our evaluation shows that the localized checking of PEQcheck can indeed be beneficial.

Wed 19 May

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

Information for Participants
Wed 19 May 2021 15:30 - 17:00 at FormaliSE Room - Program verification
Info for room FormaliSE Room:

Go directly to this room on Clowdr