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

arXiv: https://arxiv.org/abs/1903.09713 · HTML: https://mlsanity.com/paper/1903.09713/

## Key facts

- Cited by 7 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 22 Mar 2019.

## Built on by (most cited first, 7 of 7)

- [ClassInvGen: Class Invariant Synthesis using Large Language Models](https://mlsanity.com/paper/2502.18917/) (2025)
- [Enhancing Automated Loop Invariant Generation for Complex Programs with Large Language Models](https://mlsanity.com/paper/2412.10483/) (2024)
- [Quokka: Accelerating Program Verification with LLMs via Invariant Synthesis](https://mlsanity.com/paper/2509.21629/) (2025)
- [Can LLMs Enable Verification in Mainstream Programming?](https://mlsanity.com/paper/2503.14183/) (2025)
- [Program Skeletons for Automated Program Translation](https://mlsanity.com/paper/2504.07483/) (2025)
- [LLM For Loop Invariant Generation and Fixing: How Far Are We?](https://mlsanity.com/paper/2511.06552/) (2025)
- [Agentic Separation Logic Specification Synthesis](https://mlsanity.com/paper/2605.27531/) (2026)

## Abstract (arXiv)

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.