Collaborative Research: Expeditions in Computer Augmented Program Engineering (ExCAPE): Harnessing Synthesis for Software Design

点击翻译按钮获取中文摘要

Computers have revolutionized our daily lives, and yet the way we program computers has changed little in the last several decades. Software development still remains a tedious and error-prone activity. ExCAPE aims to change programming from a purely manual task to one in which a programmer and an automated program synthesis tool collaborate to generate software that meets its specification. A distinguishing feature of the ExCAPE approach is that the program description can involve a wide range of artifacts that are best-suited to the particular development task: incomplete programs; declarative specifications of high-level requirements; positive and negative examples of desired behaviors; and optimization criteria for selecting among alternative implementations. This diversity is aimed at allowing a programmer flexibility to express insights through a variety of formats, leading to a more intuitive and less error-prone way of programming.The synthesis tool uses a range of computational approaches and developer interaction to compose these different views about the structure and functionality of the system into a unified, concrete implementation. The computational techniques include decision procedures for constraint-satisfaction problems; iterative schemes for abstraction and refinement; and data-driven learning. The methodology for programmer interaction moves verification from the back-end of the design cycle to the front-end, with the promise of a more reliable software product.To develop the theory and practice of the proposed paradigm, the ExCAPE team brings together expertise in theoretical foundations (computer-aided verification, control theory, program analysis), design methodology (human-computer interaction, model-based design, programming environments), and applications (concurrent programming, network protocols, robotics, system architecture). Research will focus on developing new computational engines for transformation and integration of synthesis artifacts, and effective methods for programmer interaction and feedback. While the benefits of the ExCAPE approach will apply broadly to software development, the ExCAPE team will focus its efforts by initially targeting four challenge problems: developing efficient concurrent data structures; developing protocols for on-chip interconnection networks; developing distributed routing network protocols; and end-user programming for autonomous robots. The ExCAPE approach will be a radical departure from the way these problems are solved today. For example, for the challenge problem on concurrent programming, the planned design tool will provide smart assistance for expert programmers to produce efficient and correct code, while the proposed tool for the robotics challenge problem will let end users program robots by demonstrating example behaviors. As ExCAPE aims to affect industrial practice, design tools for all four challenge problems will be developed and evaluated in close collaboration with industrial partners.The technology developed by ExCAPE also has the potential to revolutionize the way computing concepts are taught. Building on the core technology used in program synthesis, the ExCAPE team plans to develop smart tutoring software that can analyze students? answers for conceptual errors and generate additional problems tailored to that student.. This tutoring software will be developed for representative high-school and undergraduate courses and will be made widely available. This outreach effort is aimed at attracting more students to computing disciplines by promoting a new and more appealing vision of what it means to program. ExCAPE will also nurture an inter-disciplinary community of researchers in computer-augmented programming, via an annual workshop, a biannual summer school, and a competition for synthesis tools, with associated challenge problems and benchmarks.For more information visit http://excape.cis.upenn.edu