Assertion-based Repair of Complex Data Structures

Abstract

Programmers have long used assertions to characterize properties of code. An assertion violation signals a corruption in the program state. At such a state, it is standard to terminate the program, debug it if possible, and re-execute it. We propose a new view: instead of terminating the program, use the violated assertion as a basis of repairing the state of the program and let it continue.

We present a novel algorithm to repair complex data structures. Given a structure that violates an assertion that represents its integrity constraints, our algorithm performs a systematic search based on symbolic execution to repair the structure, i.e., mutate it such that the resulting structure satisfies the given constraints. Heuristics to prune search and minimize mutations enable efficient and effective repair.

Experiments using libraries and applications, such as a naming architecture and a database engine, show that our prototype efficiently repairs complex structures while enabling systems to recover from potentially crippling errors.

Biography

Sarfraz Khurshid is an Assistant Professor in the Electrical and Computer Engineering department at the University of Texas at Austin, where he leads the Software Verification and Testing Group.