[Eecs-news-links] CIS Colloquium - Tuesday, April 12 @ University of Oregon

Batten, Tina tina.batten at oregonstate.edu
Wed Apr 6 09:43:34 PDT 2016

Begin forwarded message:

From: Adriane Bolliger <adriane at cs.uoregon.edu<mailto:adriane at cs.uoregon.edu>>
Date: April 6, 2016 at 9:38:48 AM PDT
To: "colloquia at cs.uoregon.edu<mailto:colloquia at cs.uoregon.edu>" <colloquia at cs.uoregon.edu<mailto:colloquia at cs.uoregon.edu>>, <dept at cs.uoregon.edu<mailto:dept at cs.uoregon.edu>>, <grads-mail at cs.uoregon.edu<mailto:grads-mail at cs.uoregon.edu>>
Subject: Re: CIS Colloquium - Thursday, April 7, 2016 @ 3:30pm in 220 Deschutes Hall

This colloquium presentation has been rescheduled for TUESDAY, April 12, 2016. There will be no colloquium on Thursday, April 7, 2016.

Please update your calendars accordingly.


Adriane Bolliger
Undergraduate Coordinator
Computer and Information Science Department
adriane at cs.uoregon.edu<mailto:adriane at cs.uoregon.edu>
Ph: (541) 346 - 1377, Fax: (541) 346 - 5373

120 Deschutes Hall
1202 University of Oregon
Eugene, OR 97403-1202

Office Hours: M - F, 9:00am - 12:00pm, 1:00 - 5:00pm

On Apr 5, 2016, at 8:26 AM, Adriane Bolliger <adriane at cs.uoregon.edu<mailto:adriane at cs.uoregon.edu>> wrote:

Mingsheng Ying
University of Technology, Sydney, Australia AND Tsinghua University, Beijing, China

Toward Automatic Verification of Quantum Programs


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 and quantum communication protocols?

A logic for verification of both partial correctness and total correctness of quantum programs was developed in our paper [TOPLAS'2011, art. no. 19]. The (relative) completeness of this logic was proved.

Recently, a theorem prover for automatic verification of partial correctness of quantum programs was built based on our logic [arXiv: 1601.03835].

To further develop automatic tools for verifying total correctness of quantum programs, we are working on techniques for synthesis of ranking functions that guarantee termination of quantum programs.


Mingsheng Ying is a Distinguished Professor with and the Research Director of the Center for Quantum Computation and Intelligent Systems (QCIS), Faculty of Engineering and Information Technology, University of Technology Sydney, Australia, and Cheung Kong Professor with the State Key Laboratory of Intelligent Technology and Systems, Department of Computer Science and Technology, Tsinghua University, Beijing, China.

Ying's research interests are quantum computation, programming theory, and foundations of artificial intelligence. He has published more than 100 papers in top international journals and conferences. He is the author of the books "Foundations of Quantum Programming" (Elsevier - Morgan Kaufmann 2016) and "Topology in Process Calculus: Approximate Correctness and Infinite Evolution of Concurrent Programs" (Springer-Verlag, 2001).

DATE: Thursday, April 7, 2016
TIME: 3:30 p.m. talk, refreshments following talk
PLACE: 220 Deschutes Hall (Colloquium Room), University of Oregon

For all CIS public talks, go to:

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://engr.oregonstate.edu/mailman/archives/public/eecs-news-links/attachments/20160406/1aed8c79/attachment.html>

More information about the Eecs-news-links mailing list