Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
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 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
18:30 - 19:15
|Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible|
Marius Kamp Friedrich-Alexander University Erlangen-Nürnberg, Michael Philippsen Friedrich-Alexander University Erlangen-Nürnberg (FAU)Media Attached
|Automated Repair of Heap-Manipulating Programs using Deductive Synthesis|
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 SingaporeMedia Attached
|GPURepair: Automated Repair of GPU Kernels|