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.
