Generalized Program Sketching by Abstract Interpretation and Logical Abduction
This paper presents a new approach for synthesizing missing parts from imperative programs by using abstract interpretation and logical abduction. Given a partial program with missing arbitrary expressions, our approach synthesizes concrete expressions that are strong enough to prove the assertions in the given program. Furthermore, the synthesized elements by our approach are the simplest and the weakest among all possible that guarantee the validity of assertions. In particular, we use a combination of forward and backward numerical analyses based on abstract interpretation to generate constraints that are solved by using the logical abduction technique.
We have implemented our approach in a prototype synthesis tool for C programs, and we show that the proposed approach is able to successfully synthesize arithmetic and boolean expressions for various C programs.
Sun 22 OctDisplayed time zone: Lisbon change
14:00 - 15:30
|Generalized Program Sketching by Abstract Interpretation and Logical Abduction|
Aleksandar S. Dimovski Mother Teresa University, SkopjePre-print File Attached
|Reverse Template Processing using Abstract Interpretation|
Matthieu Lemerre Université Paris-Saclay - CEA LISTPre-print
|BREWasm: A General Static Binary Rewriting Framework for WebAssemblyRemote|
Shangtong Cao Beijing University of Posts and Telecommunications, Ningyu He Peking University, Yao Guo Peking University, Haoyu Wang Huazhong University of Science and TechnologyPre-print