* ICSE 2018 *
Sun 27 May - Sun 3 June 2018 Gothenburg, Sweden
Wed 30 May 2018 16:30 - 16:45 at E3 room - Mining, Verifying, and Learning Chair(s): Mukul Prasad

Proving correctness of programs is a challenging task, and consequently has been the focus of a lot of research. One way to break this problem down is to look at one execution path of the program, argue for its correctness, and see if the argument extends to the entire program. However, that may not often be the case, i.e. the proof of a given instance can be overly specific. In this paper, we propose a technique to generalize from such specific-instance proofs, to derive a correctness argument for the entire program. The individual proofs are obtained from an off-the-shelf interpolating prover, and we use Syntax-Guided Synthesis (SyGuS) to generalize the facts that constitute those proofs. Our initial experiment with a prototype tool shows that there is a lot of scope to guide the generalization engine to converge to a proof very quickly.

Wed 30 May
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

16:00 - 17:30: Mining, Verifying, and LearningNIER - New Ideas and Emerging Results at E3 room
Chair(s): Mukul PrasadFujitsu Laboratories of America
16:00 - 16:15
Talk
NIER - New Ideas and Emerging Results
Tianyin XuUniversity of Illinois at Urbana-Champaign, Darko MarinovUniversity of Illinois at Urbana-Champaign
Pre-print
16:15 - 16:30
Talk
NIER - New Ideas and Emerging Results
Hoa Khanh DamUniversity of Wollongong, Truyen Tran, Aditya Ghose
Pre-print
16:30 - 16:45
Talk
NIER - New Ideas and Emerging Results
Muqsit Azeem, Kumar MadhukarTCS Innovation Labs (TRDDC), R Venkatesh
16:45 - 17:00
Talk
NIER - New Ideas and Emerging Results
17:00 - 17:15
Talk
NIER - New Ideas and Emerging Results
17:15 - 17:30
Short-paper
NIER - New Ideas and Emerging Results
Vasiliki EfstathiouAthens University of Economics and Business, Diomidis SpinellisAthens University of Economics and Business
DOI Pre-print