We study the problem of automatically repairing infinite-state software programs w.r.t. temporal hyperproperties. As a first step, we present a repair approach for the temporal logic HyperLTL based on symbolic execution, constraint generation, and syntax-guided synthesis of repair expression (SyGuS). To improve the repair quality, we introduce the notation of a transparent repair that aims to find a patch that is as close as possible to the original program. As a practical realization, we develop an iterative repair approach. Here, we search for a sequence of repairs that are closer and closer to the original program's behavior. We implement our method in a prototype and report on encouraging experimental results using off-the-shelf SyGuS solvers.
@article{arxiv.2408.06035,
title = {Syntax-Guided Automated Program Repair for Hyperproperties},
author = {Raven Beutner and Tzu-Han Hsu and Borzoo Bonakdarpour and Bernd Finkbeiner},
journal= {arXiv preprint arXiv:2408.06035},
year = {2024}
}