Automatic Data Structure Repair using Separation Logic

Guolong Zheng, Quang Loc Le, ThanhVu Nguyen, Quoc-Sang Phan

    Research output: Contribution to journalArticlepeer-review

    145 Downloads (Pure)

    Abstract

    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.
    Original languageEnglish
    JournalACM SigSoft Software Engineering Notes
    DOIs
    Publication statusPublished - 4 Oct 2018

    Bibliographical note

    Author retains copyright in article [https://www.sigsoft.org/SEN/subpub.html] accessed 26/9/18

    Fingerprint

    Dive into the research topics of 'Automatic Data Structure Repair using Separation Logic'. Together they form a unique fingerprint.

    Cite this