A simple inductive synthesis methodology and its applications

Given a high-level specification and a low-level programming language, our goal is to automatically synthesize an efficient program that meets the specification. In this paper, we present a new algorithm and methodology for inductive synthesis that allows us to do this. We use Second Order logic as our generic high level specification logic. For our low-level languages we choose small application-specific logics that can be immediately translated into code that runs in expected linear time in the worst case. We explain our methodology and provide examples of the synthesis of several graph classifiers, e.g, linear-time tests of whether the input graph is connected, acyclic, etc. In another set of applications we automatically derive many finite differencing expressions equivalent to ones that Paige built by hand in his thesis [Pai81]. Finally we describe directions for automatically combining such automatically generated building blocks to synthesize efficient code implementing...

• Type: Journal
• Year: 2010
• Where: OOPSLA
• Authors: Shachar Itzhaky, Sumit Gulwani, Neil Immerman, Mooly Sagiv
• Keywords: Low-level Programming Language, OOPSLA 2010, Second Order Logic, Security Privacy, Small Application-specific Logics