Syntax-Guided Automated Program Repair for Hyperproperties

TL;DR

This paper introduces a syntax-guided approach for automatically repairing infinite-state software programs with respect to hyperproperties, using symbolic execution, constraint solving, and iterative refinement to produce minimal patches.

Contribution

It presents a novel repair method for HyperLTL properties based on SyGuS, including the concept of transparent repairs and an iterative repair process to improve quality.

Findings

Prototype implementation demonstrates practical feasibility.

Encouraging experimental results with off-the-shelf SyGuS solvers.

First approach to syntax-guided repair for hyperproperties.

Abstract

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.