SPT: Storyboard Programming Tool

  • Rishabh Singh ,
  • Armando Solar-Lezama

24th International Conference on Computer Aided Verification (CAV 2012) |

We present Spt, a tool that helps programmers write low-level data-structure manipulations by combining various forms of insights such as abstract and concrete input-output examples as well as implementation skeletons. When programmers write such manipulations, they typically have a clear high-level intuition about how the manipulation should work, but implementing efficient low-level pointer manipulating code is error-prone. Our tool aims to bridge the gap between the intuition and the corresponding implementation by automatically synthesizing the implementation. The tool frames the synthesis problem as a generalization of an abstract-interpretation based shape analysis, and represents the problem as a set of constraints which are solved efficiently by the Sketch solver. We report the successful evaluation of our tool on synthesizing several linked list and binary search tree manipulations.