FMitF: Track I: Retargetable, Verifiable, Optimizable Computer-Aided Manufacturing

本项目将计算机科学形式化方法的思想应用和扩展到制造项目的设计和制造中。由于许多原因，计算机辅助制造有望对社会产生变革性的影响，包括前所未有的定制和小批量制造能力，以及更高效、更灵活的制造计划（例如，随着材料可用性的变化）。但设计师和工程师需要更灵活的工具，可以在设计阶段和制造规划阶段进行优化，并且能够适应不断变化的约束条件。该提案的新颖之处是实现这些工具的基础和原型，特别是通过设计接口，这些接口本质上是计算机科学意义上的编程语言，并且可用于正确性和优化的自动程序分析。该提案的影响包括计算机辅助制造的新语言和工具，以及制造可以自动重新定位使用不同的材料和/或工艺的演示。该项目以嵌入式系统的关键使用为中心，在形式方法和计算制造方面推进了最先进的技术。对于计算制造，该项目围绕一个中心愿景进行组织：制造是一种编译形式，将抽象的几何设计转化为等效的具体物理制造计划。通过将制造软件分解为类似编译器的抽象层，该研究可以构建自动化的、可重用的、跨领域的分析、优化和制造合成。对于正式方法，制造带来了新的挑战。它需要混合计算和几何推理，包括诸如材料既不能复制也不能从无到有的约束，以及物理对象服从重力并且不能与另一个对象占据相同的空间。其他挑战包括并发性（制造过程中多个移动部件）和物体在连续空间中移动时的数值近似。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

This project applies and extends ideas from computer science formal methods to the design and fabrication of manufactured items. Computer-aided manufacturing promises to have transformative impacts on society for many reasons, including unprecedented ability for customization and low-volume manufacturing as well as more efficient and flexible fabrication plans (e.g., as material availability changes). But designers and engineers need more flexible tools that can optimize across both the design stage and the fabrication-planning stages, and be robust to changing constraints. This proposal’s novelties are foundations and prototypes that enable such tools, in particular by designing interfaces that are essentially programming languages in the computer science sense and amenable to automated program analysis for correctness and optimization. This proposal’s impacts include new languages and tools for computer-aided manufacturing as well as demonstrations that fabrication can be automatically retargeted to use different materials and/or processes.This project advances the state-of-the-art in both formal methods and computational fabrication, centered around the critical use of embedded systems. For computational fabrication, the project is organized around a central vision: manufacturing is a form of compilation that translates abstract geometric designs to equivalent concrete physical fabrication plans. By decomposing manufacturing software into compiler-like layers of abstraction, the research enables the construction of automated, reusable,cross-domain analyses, optimizations, and synthesis for fabrication. For formal methods, manufacturing introduces new challenges. It requires mixing computational and geometric reasoning, including constraints like materials that can be neither duplicated nor created from nothing, and that physical objects obey gravity and cannot occupy the same space as another object. Additional challenges include concurrency (multiple moving parts during fabrication) and numerical approximations as objects are moved in continuous space.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.