The last ten years have seen the coming of age of a range of verification technologies to ensure that programs behave correctly according to their specifications. But checking for errors is only the first step down the road to better more reliable software. The same technology that can help us discover bugs and verify the correctness of existing software can enable a new class of programming systems that enable more natural and more declarative forms of interaction, and that may ultimately lead to better software that both more reliable and easier to produce.
This talk will describe a few of the technologies that my group has been developing to leverage program analysis technology to automate different aspects of software development. The first part of the talk will describe our recent work on "Storyboard Programming", a synthesis technique that allows programmers to describe their insight about a complex data structure manipulation by providing an abstract graphical description of how the data-structure evolves as it is manipulated. From the storyboard, our system is able to synthesize the low-level pointer updating code that is necessary to implement the desired manipulation. Storyboard Programming is an example of a new class of multimodal synthesis algorithms that are able to combine partial specifications from many different formalisms to produce a desired implementation.
The second part of the talk will describe our ongoing work on automating the enforcement of information flow policies. The goal of this project is to take a synthesis approach to information flow control: unlike a lot of related work which aims to verify that a given program satisfies a set of information flow policies, our system makes it possible to write a program without worrying about information flow, and then automatically make it satisfy a given set of policies while making only minimal changes.