查看文章

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, eg, 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.