Formal Methods in Synthetic Biology

Add to your list(s) Download to your calendar using vCal

• Boyan Yordanov, University of Boston
• Tuesday 12 April 2011, 09:20-10:20
• Large public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge.

If you have a question about this talk, please contact Microsoft Research Cambridge Talks Admins.

Synthetic biology is an emerging field focusing on the rational design of biological systems. Constructing synthetic gene networks with specific functions can lead to applications that impact our quality of life and can help elucidate the engineering principles used by nature. Even though a number of “biological devices” have already been built, the design process has so far remained challenging, forcing researchers to rely on the manual analysis of complex mathematical models and costly trial-and-error experimentation. As the field matures, systematic approaches enabling the implementation of intricate designs into functionally correct devices with little experimental work are sought.

Similar challenges have also been faced in the design of digital circuits and computer programs and various formalisms for specifying the correctness of such systems have been proposed. In addition, automatic verification and synthesis techniques have been developed to check if models such as finite transition graphs and automata satisfy these specifications or to construct correct-by-design systems. Even so, such models are often too simple to serve directly in design applications for synthetic biology. In this talk, I will discuss my efforts to bridge this gap by enabling the analysis and design of synthetic gene networks through formal verification techniques. In particular, I will describe a framework in which realistic models based on hybrid systems are constructed automatically from experimental data characterizing the different parts a device is composed of. The specific model structure guarantees that all experimental observations are captured while allowing the efficient construction of finite abstractions. The correctness of such models with respect to temporal logic specifications can then be verified automatically using methods inspired by model checking. This approach does not require numerical simulation and leads to formal guarantees of correct device behavior, while the notion of robustness (i.e. correctness under a range of model parameters) is also incorporated.

This talk is part of the Microsoft Research Machine Learning and Perception Seminars series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Guy Emerson's list
• Interested Talks
• Large public lecture room, Microsoft Research Ltd, 7 J J Thomson Avenue (Off Madingley Road), Cambridge
• ML
• Machine Learning Summary
• Microsoft Research Cambridge, public talks
• Microsoft Research Machine Learning and Perception Seminars
• Optics for the Cloud
• PMRFPS's
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• personal list
• rp587
• yk373's list

Note that ex-directory lists are not shown.