BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verification of Quantum Programs -  Mingsheng Ying (UTS Sydney)
DTSTART:20160609T130000Z
DTEND:20160609T140000Z
UID:TALK66539@talks.cam.ac.uk
CONTACT:Sergii Strelchuk
DESCRIPTION:Programming is error-prone. It is even worse when programming 
 a quantum computer or designing quantum communication protocols\, because 
 human intuition is much better adapted to the classical world than to the 
 quantum world. How can we build automatic tools for verifying correctness 
 of quantum programs? A logic for verification of both partial correctness 
 and total correctness of quantum programs was developed in our TOPLAS'2011
  paper. The (relative) completeness of this logic was proved. Recently\, a
  theorem prover for verification of quantum programs was built based on th
 is logic [arXiv: 1601.03835]. To further develop automatic tools\, we are 
 working on techniques for invariant generation and synthesis of ranking fu
 nctions (for termination analysis) of quantum programs.
LOCATION:MR14\, Centre for Mathematical Sciences\, Wilberforce Road\, Camb
 ridge
END:VEVENT
END:VCALENDAR