Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Functional Analysis of Large-scale DNA Strand Displacement Circuits

Boyan Yordanov, Christoph Wintersteiger, Youssef Hamadi, Andrew Phillips, and Hillel Kugler


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.


Publication typeArticle
Published inInternational Conference on DNA Computing and Molecular Programming
> Publications > Functional Analysis of Large-scale DNA Strand Displacement Circuits