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

协作研究：计算机增强程序工程探险 (ExCAPE)：利用综合进行软件设计

• 批准号: 1139011
• 负责人: Moshe Vardi
• 金额: $ 100万
• 依托单位: William Marsh Rice University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2012
• 资助国家: 美国
• 起止时间: 2012-04-01 至 2018-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1139011&HistoricalAwards=false
• 关键词: Collaborative; Research; Expeditions; Computer; Augmented

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

Excape：计算机增强计划工程探险PI/机构：宾夕法尼亚州大学Computers Rajeev Alur彻底改变了我们的日常生活，但是我们对计算机进行编程的方式在过去几十年中几乎没有变化。软件开发仍然仍然是一项繁琐且容易出错的活动。 Excape旨在将编程从纯粹的手动任务更改为程序员和自动化程序合成工具的协作，以生成满足其规范的软件。 Excape方法的一个显着特征是程序描述可以涉及最适合特定开发任务的广泛文物：不完整的程序；高级要求的声明规格；所需行为的积极和负面例子；以及在替代实现之间选择的优化标准。这种多样性旨在允许程序员灵活地通过各种格式表达见解，从而导致更直观，更容易出错的编程方式。综合工具使用一系列计算方法和开发人员的相互作用来构成有关系统的结构和功能的这些不同的观点，以使系统的结构和功能分解为统一的混凝土实施。计算技术包括解决约束 - 满足问题的决策程序；迭代方案用于抽象和精致；和数据驱动的学习。 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协议，机器人技术，系统体系结构）。研究将着重于开发新的计算引擎，以转换和整合合成工件，以及用于程序员互动和反馈的有效方法。尽管Excape方法的好处将广泛适用于软件开发，但Excape团队将通过最初针对四个挑战问题来集中精力：开发有效的并发数据结构；开发用于片上互连网络的协议；开发分布式路由网络协议；以及用于自动机器人的最终用户编程。 Excape方法将与今天解决这些问题的解决方式相去甚远。例如，对于并发编程中的挑战问题，计划的设计工具将为专家程序员提供高效和正确的代码提供智能帮助，而Robotics挑战问题的提议的工具将使最终用户通过演示示例行为来让最终用户编程机器人。由于Excape旨在影响工业实践，因此将与工业合作伙伴密切合作开发和评估所有四个挑战问题的设计工具。Excape开发的技术还具有彻底改变计算概念的方式。在计划合成中使用的核心技术的基础上，Excape团队计划开发可以分析学生的智能辅导软件？概念错误的答案并为该学生量身定制的其他问题。该辅导软件将用于代表性的高中和本科课程，并将广泛使用。这种推广工作旨在通过促进对编程意味着什么，吸引更多的学生来计算学科。 Excape还将通过年度研讨会，一年一度的暑期学校和合成工具的竞争来培养一个在计算机调节节目中的研究人员的跨学科社区，并提供了相关的挑战问题和基准。有关更多信息，请访问http://excape.cis.upenn.eduu