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

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

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.