Date Added: May 2010
The authors present a novel approach to automatic synthesis of loop-free programs. The approach is based on a combination of oracle-guided learning from examples, and constraint-based synthesis from components using Satisfiability Modulo Theories (SMT) solvers. The authors' approach is suitable for many applications, including as an aid to program understanding tasks such as deobfuscating malware. They demonstrate the efficiency and effectiveness of their approach by synthesizing bitmanipulating programs and by deobfuscating programs. Automatic synthesis of programs has long been one of the holy grails of software engineering. It has found many practical applications: generating optimal code sequences, optimizing performance-critical inner loops, generating general-purpose peephole optimizers, automating repetitive programming tasks, and filling in low-level details after the higher-level intent has been expressed.