BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Formal Methods in Synthetic Biology - Boyan Yordanov\, University 
 of Boston
DTSTART:20110412T082000Z
DTEND:20110412T092000Z
UID:TALK30765@talks.cam.ac.uk
CONTACT:Microsoft Research Cambridge Talks Admins
DESCRIPTION:Synthetic biology is an emerging field focusing on the rationa
 l design of biological systems. Constructing synthetic gene networks with 
 specific functions can lead to applications that impact our quality of lif
 e and can help elucidate the engineering principles used by nature. Even t
 hough a number of “biological devices” have already been built\, the d
 esign process has so far remained challenging\, forcing researchers to rel
 y on the manual analysis of complex mathematical models and costly trial-a
 nd-error experimentation. As the field matures\, systematic approaches ena
 bling the implementation of intricate designs into functionally correct de
 vices with little experimental work are sought.\n\nSimilar challenges have
  also been faced in the design of digital circuits and computer programs a
 nd various formalisms for specifying the correctness of such systems have 
 been proposed. In addition\, automatic verification and synthesis techniqu
 es have been developed to check if models such as finite transition graphs
  and automata satisfy these specifications or to construct correct-by-desi
 gn systems. Even so\, such models are often too simple to serve directly i
 n design applications for synthetic biology.\nIn this talk\, I will discus
 s my efforts to bridge this gap by enabling the analysis and design of syn
 thetic gene networks through formal verification techniques. In particular
 \, I will describe a framework in which realistic models based on hybrid s
 ystems 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 suc
 h models with respect to temporal logic specifications can then be verifie
 d automatically using methods inspired by model checking. This approach do
 es not require numerical simulation and leads to formal guarantees of corr
 ect device behavior\, while the notion of robustness (i.e. correctness und
 er a range of model parameters) is also incorporated. \n
LOCATION:Large public lecture room\, Microsoft Research Ltd\, 7 J J Thomso
 n Avenue (Off Madingley Road)\, Cambridge
END:VEVENT
END:VCALENDAR