Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Sun 13 Jan 2019 15:00 - 15:30 at Sala III - Program Synthesis Chair(s): Nuno P. Lopes

We present an automated approach to repair programs using formal verification and expression templates. In our approach, an input program is first verified against its formal specification to discover potentially buggy statements. For each of these statements, we identify the expression that needs to be repaired and set up a template patch which is a linear expression composed of the program’s variables and unknown coefficients. Then, we analyze the template-patched program against its specification to collect a set of constraints of the template patch. This constraint set will be solved by a constraint solving technique using Farkas’ lemma to identify the unknown coefficients, consequently discovering the patch. We implement our approach in a tool called Maple and evaluate it with various buggy programs from a widely used benchmark TCAS as well as a synthetic, yet challenging benchmark containing recursive programs. Our tool outperforms state-of-the-art program repair tools in returning desired patches.

Sun 13 Jan

14:00 - 15:30: VMCAI 2019 - Program Synthesis at Sala III
Chair(s): Nuno P. LopesMicrosoft Research
VMCAI-201914:00 - 14:30
Jad HamzaLIAFA, Université Paris Diderot, Viktor KuncakEPFL, Switzerland
VMCAI-201914:30 - 15:00
Grigory FedyukovichPrinceton University, Arie GurfinkelUniversity of Waterloo, Aarti GuptaPrinceton University
VMCAI-201915:00 - 15:30
Thanh-Toan Nguyen, Quang-Trung TaNational University of Singapore, Wei-Ngan ChinNational University of Singapore