A Caltech Library Service

Compiling and Verifying DNA-Based Chemical Reaction Network Implementations


Shin, Seung Woo (2012) Compiling and Verifying DNA-Based Chemical Reaction Network Implementations. Master's thesis, California Institute of Technology. doi:10.7907/QM4N-KX17.


One goal of molecular programming and synthetic biology is to build chemical circuits that can control chemical processes at the molecular level. Remarkably, it has been shown that synthesized DNA molecules can be used to construct complex chemical circuits that operate without any enzyme or cellular component. However, designing DNA molecules at the individual nucleotide base level is often difficult and laborious, and thus chemical reaction networks (CRNs) have been proposed as a higher-level programming language. So far, several general-purpose schemes have been described for designing synthetic DNA molecules that simulate the behavior of arbitrary CRNs, and many more are being actively investigated.

Here, we solve two problems related to this topic. First, we present a general-purpose CRN-to-DNA compiler that can apply user-defined compilation schemes for translating formal CRNs to domain-level specifications for DNA molecules. In doing so, we develop a language in which such schemes can be concisely and precisely described. This compiler can greatly reduce the amount of tedious manual labor faced by researchers working in the field. Second, we present a general method for the formal verification of the correctness of such compilation. We first show that this problem reduces to testing a notion of behavioral equivalence between two CRNs, and then we construct a mathematical formalism in which that notion can be precisely defined. Finally, we provide algorithms for testing that notion. This verification process can be thought of as an equivalent of model checking in molecular computation, and we hope that the generality of our verification techniques will eventually allow us to apply them not only to DNA-based CRN implementations but to a wider class of molecular programs.

Item Type:Thesis (Master's thesis)
Subject Keywords:DNA computation; compiler; software verification; model checking
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computer Science
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Winfree, Erik
Thesis Committee:
  • Unknown, Unknown
Defense Date:2011
Non-Caltech Author Email:seungwoo.theory (AT)
Funding AgencyGrant Number
Caltech Computer Science dept. UNSPECIFIED
Record Number:CaltechTHESIS:09182011-215125061
Persistent URL:
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:6676
Deposited By: Seung Woo Shin
Deposited On:19 Sep 2011 19:17
Last Modified:03 Oct 2019 23:53

Thesis Files

[img] PDF (Complete Thesis) - Final Version
See Usage Policy.


Repository Staff Only: item control page