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 JunDisplayed time zone: Tijuana, Baja California change
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 20mTalk | 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 20mTalk | 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 20mTalk | 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 20mTalk | 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 |