Generalizing Specific-Instance Interpolation Proofs with SyGuS
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 MayDisplayed 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 Prasad Fujitsu Laboratories of America | ||
16:00 15mTalk | Mining Container Image Repositories---MSR for Software Configurations and Beyond NIER - New Ideas and Emerging Results Tianyin Xu University of Illinois at Urbana-Champaign, Darko Marinov University of Illinois at Urbana-Champaign Pre-print | ||
16:15 15mTalk | Explainable Software Analytics NIER - New Ideas and Emerging Results Pre-print | ||
16:30 15mTalk | Generalizing Specific-Instance Interpolation Proofs with SyGuS NIER - New Ideas and Emerging Results | ||
16:45 15mTalk | Efficient Parametric Model Checking Using Domain-Specific Modelling Patterns NIER - New Ideas and Emerging Results | ||
17:00 15mTalk | Deep Learning UI Design Patterns of Mobile Apps NIER - New Ideas and Emerging Results | ||
17:15 15mShort-paper | Code Review Comments: Language matters NIER - New Ideas and Emerging Results Vasiliki Efstathiou Athens University of Economics and Business, Diomidis Spinellis Athens University of Economics and Business DOI Pre-print |