Collaborative Research: SHF: Small: Interactive Synthesis and Repair For Robot Programs

在过去的几年里，机器人已经开始部署在非结构化的人类环境中。有数百个机器人部署在医院、酒店和超市。不幸的是，在机器人上运行的软件是使用低级抽象和语言编程的，很难在机器人和环境之间进行转移。此外，机器人软件需要复杂的控制逻辑，以确保机器人在所有情况下都是安全和行为良好的。因此，机器人软件非常难以编写和维护。这个研究项目开发工具和技术，使机器人软件更安全，更容易编写，更容易维护。该项目的智力优势在于：(1)基于自动程序修复和程序合成的进步，开发了修复机器人软件缺陷的技术；(2)基于新的编程语言设计，编写能够自动处理某些类型故障的机器人软件的抽象；(3)基于新的程序验证技术的机器人软件正确性检验方法。该项目更广泛的意义和重要性在于，它有助于使机器人软件更容易编写和维护，更便宜、更安全、更可靠。该项目通过发布研究成果和发布开源软件，鼓励在编程语言和机器人技术的交叉领域进行进一步研究。该项目还包括高中外展研讨会，以扩大对计算机的参与。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Over the past few years, robots have started to be deployed in unstructured human environments. There are hundreds of robots deployed in hospitals, hotels, and supermarkets. Unfortunately, the software that runs on robots is programmed using low-level abstractions and languages, and is hard to transfer across robots and environments. In addition robotic software requires complex control logic to ensure that robots are safe and well-behaved in all situations. Thus, robot software is extraordinarily hard to write and maintain. This research project develops tools and techniques to make robot software safer, easier to write, and easier to maintain. The intellectual merits of the project are the development of (1) techniques for fixing bugs in robot software, based on advances to automatic program repair and program synthesis; (2) abstractions for writing robot software that can automatically handle certain kinds of failures, based on new programming-language design; (3) methods for checking the correctness of robot software, based on new program-verification techniques. The project's broader significance and importance are that it helps make robot software easier to write and maintain, and cheaper, safer, and more reliable. The project encourages further research at the intersection of programming languages and robotics by publishing research results and releasing open-source software. The project also involves high-school outreach workshops to broaden participation in computing.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.