According to a recent observational study, developers spend an average of 48% of their development time on debugging tasks. Approaches such as equivalence checking and fault localization support developers during debugging tasks by providing information that enables developers to more quickly identify and deal with unintended changes in program behavior. The accuracy and runtime performance of these approaches have seen continuous improvements throughout the years. However, the outputs of existing tools are often difficult to understand for developers due to a lack of context information and result explanations. Our goal is to improve upon this issue by developing a new equivalence checking approach that (i) is at least as accurate as existing approaches but (ii) provides more detailed descriptions of identified behavioral / semantic differences and (iii) presents these results in a way that is useful for developers, thus aiding developer understanding of equivalence checking results and corresponding software changes.

Johann Glock is a Ph.D. student in the Software Engineering Research Group (SERG) at the University of Klagenfurt, Austria. He received his M.Sc. in software engineering at the University of Applied Sciences Upper Austria, Campus Hagenberg, Austria in 2020. His research interests are in program analysis, program comprehension, and formal methods.