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

例外：计算机增强程序工程的探险领导PI/机构：拉吉夫·阿鲁尔，宾夕法尼亚大学计算机已经彻底改变了我们的日常生活，然而在过去的几十年里，我们为计算机编程的方式几乎没有改变。软件开发仍然是一项乏味且容易出错的活动。ExCAPE旨在将编程从纯手工任务转变为程序员和自动程序合成工具协作生成符合其规范的软件的任务。ExCAPE方法的一个显著特征是程序描述可以包含范围广泛的最适合特定开发任务的工件：不完整的程序；高层次需求的声明性规范；期望行为的正面和负面例子；以及在备选实现中进行选择的优化标准。这种多样性旨在允许程序员通过各种格式灵活地表达见解，从而实现更直观、更不易出错的编程方式。综合工具使用一系列计算方法和开发人员交互，将这些关于系统结构和功能的不同视图组合成一个统一的、具体的实现。计算技术包括约束满足问题的决策过程；抽象和细化的迭代方案；以及数据驱动的学习。程序员交互的方法将验证从设计周期的后端移动到前端，从而保证了更可靠的软件产品。为了发展提出的范例的理论和实践，ExCAPE团队汇集了理论基础（计算机辅助验证、控制理论、程序分析）、设计方法（人机交互、基于模型的设计、编程环境）和应用（并发编程、网络协议、机器人、系统架构）方面的专业知识。研究将集中于开发新的计算引擎，用于合成工件的转换和集成，以及程序员交互和反馈的有效方法。虽然ExCAPE方法的好处将广泛应用于软件开发，但ExCAPE团队将集中精力，首先针对四个挑战问题：开发高效的并发数据结构；开发片上互连网络协议；开发分布式路由网络协议；以及自主机器人的终端用户编程。escape的方法将彻底改变目前解决这些问题的方式。例如，对于并发编程的挑战问题，规划的设计工具将为专家程序员提供智能帮助，以生成高效和正确的代码，而针对机器人挑战问题提出的工具将让最终用户通过演示示例行为来编程机器人。由于ExCAPE旨在影响工业实践，因此将与工业伙伴密切合作，开发和评估所有四个挑战问题的设计工具。ExCAPE开发的技术也有可能彻底改变计算机概念的教学方式。ExCAPE团队计划以程序合成中使用的核心技术为基础，开发能够分析学生行为的智能辅导软件。概念错误的答案，并为该学生量身定制额外的问题。该辅导软件将针对具有代表性的高中和大学课程开发，并将广泛使用。这种拓展努力的目的是通过推广一种新的、更吸引人的编程方式来吸引更多的学生进入计算机学科。ExCAPE还将通过每年一次的研讨会、一年两次的暑期学校和综合工具竞赛，以及相关的挑战问题和基准，培养一个计算机增强编程领域的跨学科研究人员社区。更多信息请访问http://excape.cis.upenn.edu

ExCAPE: Expeditions in Computer Augmented Program EngineeringLead PI/Institution: Rajeev Alur, University of PennsylvaniaComputers 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