The sequence-specific nature of DNA hybridization makes it an ideal framework for programming structure and dynamics at the nanoscale. We engineer DNA strand displacement networks to implement molecular logic gates, sensors, and adaptive systems. We focus in particular on exploiting DNA chirality in circuit design, which is the topic of Dr. Lakin's NSF CAREER project. We also work on the design of tethered molecular circuits that are spatially localized to a DNA surface. This work has potential applications in the development of diagnostic bioassays and in the autonomous diagnosis and treatment of disease.
Designing genetic circuits enables us to program the behavior of living organisms. For example, engineered RNAs can be used as switches to interface with protein-based transcriptional control via CRISPR/Cas systems. We work on prototyping novel genetic regulatory motifs in cell-free transcription/translation systems and on realizing these in living cells and in synthetic cells. We also work on the implementation of adaptive behaviors in engineered cells.
Engineering biological systems involves creating abstractions that can be formalized as domain-specific modeling languages. These enable models to be specified in a precise manner and then automatically translated into an executable format by applying semantic compilation rules. We work on the design and implementation of programming languages for modeling and simulating a range of systems in biomolecular computing and nanotechnology. Dr. Lakin has previously worked on a number of biological modeling languages, including Visual DSD, Genetic Engineering of Cells, and the Stochastic Pi Machine.
A key advantage of specifying models in a formal language is that they can then be formally verified using computer-aided reasoning techniques. We work on developing such techniques for proving the correctness of programs specified as abstract chemical reaction networks, and on applying automated techniques such as model checking and satisfiability modulo theories solving to analyze the behavior of biomolecular systems. We are also interested in formal verification of the scientific software that forms the basis of biological modeling workflows.