# SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic

## TL;DR

SLING is a dynamic analysis tool that infers separation logic invariants for heap-manipulating programs by analyzing execution traces and memory regions, aiding in understanding program behavior.

## Contribution

Introduces SLING, a novel dynamic analysis method that automatically generates separation logic invariants from execution traces of C programs.

## Key findings

- Efficiently generates correct invariants for complex data structures
- Works at arbitrary program locations like preconditions and loop invariants
- Preliminary results show effectiveness on existing benchmarks

## Abstract

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.