Research

In general, my interests lie in applying formal verification methods to systems in a variety of disciplines.

I am currently working on the Bio Cyberphysical Systems (BioCPS) for Engineering Living Cells project. The goal of this project is to create a next-generation Cyberphysical System that is capable of engineering populations of bacterial (primarily E. coli) and mammalian (primarily Chinese hamster ovary and human-induced pluripotent stem) cells to produce “desired” patterns. My focus in the project is to solve a functional synthesis problem, which involves synthesizing a genetic circuit from a library of well-characterized modules that implements a desired specification given in signal temporal logic (STL). To address this problem, I am working on Phoenix, a tool that assists users in an iterative, hierarchical specify-design-build-test cycle for constructing genetic circuits.

I have developed a couple metrics for computing the distance between two STL formulae, which can be used to check how close a derived specification is to a desired specification. Additionally, I have been involved in the development of STL#, an extension to STL that includes syntax and semantics for composition of temporal logic formulae. Using STL#, a designer can computationally compose STL formulae together hierarchically.  Currently, I am looking into different methods for exploring the design space of a genetic circuit given a library of modules.