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

In this paper, we present a novel learning framework for inferring stateful preconditions (i.e., preconditions constraining not only primitive-type inputs but also non-primitive-type object states) modulo a test generator, where the quality of the preconditions is based on their safety and maximality with respect to the test generator. We instantiate the learning framework with a specific learner and test generator to realize a precondition synthesis tool for C#. We use an extensive evaluation to show that the tool is highly effective in synthesizing preconditions for avoiding exceptions as well as synthesizing conditions under which methods commute.

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