  We introduce a new dynamic analysis technique to discover invariants in
separation logic for heap-manipulating programs. First, we use a debugger to
obtain rich program execution traces at locations of interest on sample inputs.
These traces consist of heap and stack information of variables that point to
dynamically allocated data structures. Next, we iteratively analyze separate
memory regions related to each pointer variable and search for a formula over
predefined heap predicates in separation logic to model these regions. Finally,
we combine the computed formulae into an invariant that describes the shape of
explored memory regions.
  We present SLING, a tool that implements these ideas to automatically
generate invariants in separation logic at arbitrary locations in C programs,
e.g., program pre and postconditions and loop invariants. Preliminary results
on existing benchmarks show that SLING can efficiently generate correct and
useful invariants for programs that manipulate a wide variety of complex data
structures.
