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