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.