FMitF: Track I: Correct-by-Construction Synthesis of Microfluidic Chips

微流体和芯片实验室技术的蓬勃发展使化学和生命科学实验的小型化和自动化成为可能，这可能会极大地提高药物发现和生物技术等关键领域的效率。然而，设计微流控芯片和实施相关软件目前需要大量的手工，容易出错的工作，抵消了该技术带来的一些生产力收益。本项目研究自动合成完整和正确的微流控芯片系统的算法。该项目的新颖之处在于，它旨在成为第一个同时合成可编程机械物体（在这种情况下，是一个微流控芯片）并结合控制它的软件的项目，包括定制芯片设计，以满足特定研究人员实验室设备的限制。该项目的影响是它拓宽了微流控技术的可用性，催化了新的微流控应用，新的跨学科研究，以及微流控的新的商业机会。在微流控芯片的形式化方法和设计自动化的大背景下，该项目旨在产生第一个合成结构正确的微流控元件、多组分微流控芯片和微流控控制程序的技术。该项目研究了一种新的反例引导感应微流控合成（CEGIMS）算法，其中微流控芯片合成器和控制程序合成器相结合，协同生成微流控芯片设计和相应的控制软件。用户提供微流体芯片几何形状和控制软件结构的草图，以及指定用户对芯片内部流动流体的物理特性的期望的评估标准。CEGIMS将物理建模软件与可满足模理论（SMT）求解器集成在一起，依靠反例引导的搜索方法来完成草图，从而产生适合制造的最终芯片布局。同时，CEGIMS自动合成控制软件，保证芯片的正确驱动。为了实现这些技术目标，该项目旨在开发基本的技术进步，将基于逻辑正确性的求解器与确定物理模型正确性的仿真软件集成在一起。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

The burgeoning field of microfluidics and laboratory-on-a-chip technologies enables miniaturization and automation of chemical and life-science experiments, potentially yielding dramatic efficiency improvements for critical fields like drug discovery and biotechnology. However, designing a microfluidic chip and implementing the associated software currently requires a great deal of manual, error-prone work, negating some of the productivity gains from the technology. This project investigates algorithms that automatically synthesize complete and correct microfluidic chip systems. The project’s novelties are that it aims to be the first to simultaneously synthesize a programmable mechanical object (in this case, a microfluidic chip) in conjunction with the software that controls it, including customization of the chip design to meet the constraints imposed by the equipment in a specific researcher’s laboratory. The project’s impacts are that it broadens the usability of microfluidic technologies, catalyzing new microfluidic applications, new interdisciplinary research, and new commercial opportunities for microfluidics.Within the larger context of formal methods and design automation for microfluidic chips, the project aims to produce the first techniques to synthesize correct-by-construction microfluidic components, multi-component microfluidic chips, and control programs for microfluidics. The project investigates a novel counterexample-guided inductive microfluidic synthesis (CEGIMS) algorithm, in which a microfluidic-chip synthesizer and a control program synthesizer are combined to synergistically generate both a microfluidic chip design and the corresponding control software for available equipment. Users provide sketches of both the microfluidic-chip geometry and control-software structure, along with evaluation criteria specifying the user’s expectations for the physical properties of the fluid flowing inside of the chip. CEGIMS integrates physical-modeling software with Satisfiability Modulo Theory (SMT) solvers, relying on counterexample-guided search methods to complete the sketches, yielding a final chip layout suitable for fabrication. At the same time, CEGIMS automatically synthesizes control software that is guaranteed to drive the chip correctly. In order to achieve these technical goals, the project aims to develop fundamental advances in techniques to integrate solvers based on logical correctness properties with simulation software that determines the correctness of a physical model.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.