Write a Blog >>
POPL 2021
Sun 17 - Fri 22 January 2021 Online
Mon 18 Jan 2021 18:45 - 19:00 at VMCAI - Synthesis and Repair Chair(s): Aws Albarghouthi

We propose a novel method to automatically repairing buggy heap-manipulating programs using constraint solving and deductive synthesis. Given an input program C and its formal specification in the form of a Hoare triple: {P} C {Q}, we use a separation-logic-based verifier to verify if program C is correct w.r.t. its specifications. If program C is found buggy, we then repair it in the following steps. First, we rely on the verification results to collect a list of suspicious statements of the buggy program. For each suspicious statement, we temporarily replace it with a template patch representing the desired statements. The template patch is also formally specified using a pair of unknown pre- and postcondition. Next, we use the verifier to analyze the temporarily patched program to collect constraints related to the pre- and postcondition of the template patch. Then, these constraints are solved by our constraint solving technique to discover the suitable specifications of the template patch. Subsequently, these specifications can be used to synthesize program statements of the template patch, consequently creating a candidate program. Finally, if the candidate program is validated, it is returned as the repaired program. We demonstrate the effectiveness of our approach by evaluating our implementation and a state-of-the-art approach on a benchmark of 231 buggy programs. The experiment results show that our tool successfully repairs 223 buggy programs and considerably outperforms the compared tool.

Mon 18 Jan

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:15
Synthesis and RepairVMCAI at VMCAI
Chair(s): Aws Albarghouthi University of Wisconsin-Madison, USA
18:30
15m
Talk
Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
VMCAI
Marius Kamp Friedrich-Alexander University Erlangen-Nürnberg, Michael Philippsen Friedrich-Alexander University Erlangen-Nürnberg (FAU)
Media Attached
18:45
15m
Talk
Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
VMCAI
Thanh-Toan Nguyen National University of Singapore, Quang-Trung Ta National University of Singapore, Ilya Sergey Yale-NUS College and National University of Singapore, Wei-Ngan Chin National University of Singapore
Media Attached
19:00
15m
Talk
GPURepair: Automated Repair of GPU Kernels
VMCAI
Saurabh Joshi IIT Hyderabad, Gautam Muduganti IIT Hyderabad
Media Attached