Functional Analysis of Large-Scale DNA Strand Displacement Circuits
We present a method for the analysis of functional properties of large-scale DNA strand displacement (DSD) circuits based on Satisfiability Modulo Theories that enables us to prove the functional correctness of DNA circuit designs for arbitrary inputs, and provides significantly improved scalability and expressivity over existing methods. We implement this method as an extension to the Visual DSD tool, and use it to formalize the behavior of a 4-bit square root circuit, together with the components used for its construction. We show that our method successfully verifies that certain designs function as required and identifies erroneous computations in others, even when millions of copies of a circuit are interacting with each other in parallel. Our method is also applicable in the verification of properties for more general chemical reaction networks.
Unable to display preview. Download preview PDF.
- 5.Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252. ACM (1977)Google Scholar
- 7.Dong, Q.: A bisimulation approach to verification of molecular implementations of formal chemical reaction networks. Master’s thesis, Stony Brook University (2012)Google Scholar
- 8.Doty, D., Hajiaghayi, M.: Leaderless deterministic chemical reaction networks. arXiv:1304.4519 (2013)Google Scholar
- 12.Kaivola, R., Ghughal, R., Narasimhan, N., Telfer, A., Whittemore, J., Pandav, S., Slobodová, A., Taylor, C., Frolov, V., Reeber, E., Naik, A.: Replacing Testing with Formal Verification in Intel® CoreTM i7 Processor Execution Engine Validation. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 414–429. Springer, Heidelberg (2009)CrossRefGoogle Scholar
- 16.Manna, Z., Pnueli, A.: Temporal verification of reactive systems: safety, vol. 2. Springer (1995)Google Scholar
- 18.Shin, S.W.: Compiling and verifying DNA-based chemical reaction network implementations. Master’s thesis, California Institute of Technology (2012)Google Scholar
- 22.Z34Bio at rise4fun Software Engineering Tools from Microsoft Research (2013), http://rise4fun.com/z34biology