Automatic Data Structure Repair using Separation Logic

Software systems are often shipped and deployed with both known and
unknown bugs. On-the-fly program repairs, which handle runtime errors
and allow programs to continue successfully, can help software reliability,
e.g., by dealing with inconsistent or corrupted data without interrupting
the running program.
We report on our work-in-progress that repairs data structure using separation
logic. Our technique, inspired by existing works on specificationbased
repair, takes as input a specification written in a separation logic
formula and a concrete data structure that fails that specification, and performs
on-the-fly repair to make the data conforms with the specification.
The use of separation logic allows us to compactly and precisely represent
desired properties of data structures and use existing analyses in
separation logic to detect and repair bugs in complex data structures.
We have developed a prototype, called STARFIX, to repair invalid Java
data structures violating given specifications in separation logic. Preliminary
results show that tool can efficiently detect and repair inconsistent
data structures including lists and trees.