Designing better and faster DNA circuits

Oxford researchers have been awarded a Microsoft Research PhD Scholarship to fund new research into automated verification techniques for DNA computing.

Oxford’s Marta Kwiatkowska, in collaboration with Oxford Physics Professor Andrew Turberfield and Microsoft Research Cambridge’s Andrew Phillips will develop new techniques and tools to help scientists design correct and efficient DNA computing designs.

DNA computing is a new and fast-growing field that aims to engineer artificial computing devices using bio-molecular materials such as DNA.

Inspired by the pioneering experiments of Leonard Adleman in the mid 90s, who used DNA to solve simple computation problems, researchers have succeeded in assembling increasingly complex nanometre-scale devices. The technology has exciting applications in the development of programmable molecular devices for use in bio-sensing and drug delivery. The new research project will develop techniques for formal verification of DNA computation and assembly designs. Formal verification methods apply rigorous, mathematical reasoning to ascertain the correctness of computerised systems. These are built into efficient software tools such as model checkers, which allow push-button use of verification technology.

The project will have a particular emphasis on quantitative verification techniques, which can be used to analyse properties such as the efficiency and reliability of DNA designs. This will build on PRISM, a software tool developed in Marta’s group, for quantitative verification of systems with probabilistic behaviour. PRISM has already been applied to many diverse systems, from wireless communications protocols such as Bluetooth, to quantum cryptography algorithms, to biological signalling pathways.

The project will design new modelling languages and verification techniques for DNA computation designs and build them into new software tools. The techniques developed will be validated against experimental data from state-of-the-art DNA assembly/computation methods, performed in the Turberfield Lab at Oxford.