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

Bit-vector-based program synthesis is an important building block of state-of-the-art techniques in computer programming. Some of these techniques do not only rely on a synthesizer’s ability to return an appropriate program if it exists but also require a synthesizer to detect if there is no such program at all in the entire search space (i.e., the problem is infeasible), which is a computationally demanding task.

In this paper, we propose an approach to quickly identify some synthesis problems as infeasible. We observe that a specification function encodes dependencies between input and output bits that a correct program must satisfy. To exploit this fact, we present approximate analyses of essential bits and use them in two novel algorithms to check if a synthesis problem is infeasible. Our experiments show that adding our technique to applications of bit vector synthesis can save up to 33% of their time.

Mon 18 Jan
Times are displayed in time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

18:30 - 19:15: Synthesis and RepairVMCAI at VMCAI
Chair(s): Aws AlbarghouthiUniversity of Wisconsin-Madison, USA
18:30 - 18:45
Talk
Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
VMCAI
Marius KampFriedrich-Alexander University Erlangen-Nürnberg, Michael PhilippsenFriedrich-Alexander University Erlangen-Nürnberg (FAU)
Media Attached
18:45 - 19:00
Talk
Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
VMCAI
Thanh-Toan NguyenNational University of Singapore, Quang-Trung TaNational University of Singapore, Ilya SergeyYale-NUS College and National University of Singapore, Wei-Ngan ChinNational University of Singapore
Media Attached
19:00 - 19:15
Talk
GPURepair: Automated Repair of GPU Kernels
VMCAI
Saurabh JoshiIIT Hyderabad, Gautam MudugantiIIT Hyderabad
Media Attached