Modelling and verification of DNA programs
DNA molecules can be used to perform complex logical computation. DNA computation differs from conventional digital computation
and is sometimes referred to as ‘computing with soup’ http://www.economist.com/node/21548488. Correct design of DNA devices
is error-prone and the task is supported by tools such as the DNA Strand Displacement (DSD) programming language and simulator
(http://research.microsoft.com/en-us/projects/dna/default.aspx) developed at Microsoft. The DSD tool enables the probabilistic
model checking of DNA circuits and has been used to identify a flaw in a DNA transducer gate (see http://qav.comlab.ox.ac.uk/bibitem.php?key=LPC+12).
The aim of this project is to model and analyse DNA implementation of logic inference proposed in “Autonomous Resolution Based
on DNA Strand Displacement”, DNA Computing and Molecular Programming, LNCS 6937, 2011. The project will suit a student interested
in modelling DNA programs using DSD and/or PRISM. For more information about the DNA computing project see http://www.veriware.org/dna.php.