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
Times are displayed in time zone: Tijuana, Baja California change

14:00 - 15:30: Learning SpecificationsPLDI Research Papers at 228AB
Chair(s): Michael PradelTU Darmstadt and Facebook
14:00 - 14:20
Talk
PLDI Research Papers
Jan EberhardtDeepCode, Switzerland, Samuel SteffenETH Zurich, Switzerland, Veselin RaychevDeepCode AG, Martin VechevETH Zürich
Pre-print Media Attached
14:20 - 14:40
Talk
PLDI Research Papers
Victor ChibotaruDeepCode, Switzerland, Benjamin BichselETH Zurich, Switzerland, Veselin RaychevDeepCode AG, Martin VechevETH Zürich
Pre-print Media Attached
14:40 - 15:00
Talk
PLDI Research Papers
Angello Astorga, P. MadhusudanUniversity of Illinois at Urbana-Champaign, Shambwaditya Saha, Shiyu WangUniversity of Illinois at Urbana-Champaign, USA, Tao XieUniversity of Illinois at Urbana-Champaign, USA
15:00 - 15:20
Talk
PLDI Research Papers
Ton Chanh LeStevens Institute of Technology, Guolong ZhengUniversity of Nebraska Lincoln, ThanhVu NguyenUniversity of Nebraska-Lincoln