Tue 25 Jun 2019 15:00 - 15:20 at 228AB - Learning Specifications Chair(s): Michael Pradel

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.

Tue 25 Jun

Displayed time zone: Tijuana, Baja California change

14:00 - 15:30
Learning SpecificationsPLDI Research Papers at 228AB
Chair(s): Michael Pradel TU Darmstadt and Facebook
14:00
20m
Talk
Unsupervised Learning of API Aliasing Specifications
PLDI Research Papers
Jan Eberhardt DeepCode, Switzerland, Samuel Steffen ETH Zurich, Switzerland, Veselin Raychev DeepCode AG, Martin Vechev ETH Zürich
Pre-print Media Attached
14:20
20m
Talk
Scalable Taint Specification Inference with Big Code
PLDI Research Papers
Victor Chibotaru DeepCode, Switzerland, Benjamin Bichsel ETH Zurich, Switzerland, Veselin Raychev DeepCode AG, Martin Vechev ETH Zürich
Pre-print Media Attached
14:40
20m
Talk
Learning Stateful Preconditions Modulo a Test Generator
PLDI Research Papers
Angello Astorga , P. Madhusudan University of Illinois at Urbana-Champaign, Shambwaditya Saha , Shiyu Wang University of Illinois at Urbana-Champaign, USA, Tao Xie University of Illinois at Urbana-Champaign, USA
15:00
20m
Talk
SLING: Using Dynamic Analysis to Infer Program Invariants in Separation Logic
PLDI Research Papers
Ton Chanh Le Stevens Institute of Technology, Guolong Zheng University of Nebraska Lincoln, ThanhVu Nguyen University of Nebraska-Lincoln