Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
Kamp M, Philippsen M (2021)
Publication Language: English
Publication Status: Submitted
Publication Type: Conference contribution, Original article
Future Publication Type: Conference contribution
Publication year: 2021
Publisher: Springer International Publishing
Series: Lecture Notes in Computer Science (LNCS)
City/Town: Cham
Book Volume: 12597
Pages Range: 353 - 375
Conference Proceedings Title: Verification, Model Checking, and Abstract Interpretation (VMCAI 2021)
Event location: Copenhagen
ISBN: 978-3-030-67066-5
URI: https://i2git.cs.fau.de/i2public/publications/-/raw/master/vmcai2021.pdf
DOI: 10.1007/978-3-030-67067-2_16
Abstract
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.
Authors with CRIS profile
Marius Kamp
Lehrstuhl für Informatik 2 (Programmiersysteme)
Michael Philippsen
Lehrstuhl für Informatik 2 (Programmiersysteme)
Related research project(s)
How to cite
APA:
Kamp, M., & Philippsen, M. (2021). Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible. In Fritz Henglein, Sharon Shoham, Yakir Vizel (Eds.), Verification, Model Checking, and Abstract Interpretation (VMCAI 2021) (pp. 353 - 375). Copenhagen, DK: Cham: Springer International Publishing.
MLA:
Kamp, Marius, and Michael Philippsen. "Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible." Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'2021), Copenhagen Ed. Fritz Henglein, Sharon Shoham, Yakir Vizel, Cham: Springer International Publishing, 2021. 353 - 375.
BibTeX: Download