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
|14:00 - 14:20|
Jan EberhardtDeepCode, Switzerland, Samuel SteffenETH Zurich, Switzerland, Veselin RaychevDeepCode AG, Martin VechevETH ZürichPre-print Media Attached
|14:20 - 14:40|
Victor ChibotaruDeepCode, Switzerland, Benjamin BichselETH Zurich, Switzerland, Veselin RaychevDeepCode AG, Martin VechevETH ZürichPre-print Media Attached
|14:40 - 15:00|
|15:00 - 15:20|