报告题目: Formal Verification of Quantum Protocols

报 告 人：邓玉欣 教授

报告时间：2022年9月27日（星期二）15:00-17:00

腾讯会议：133-192-704

报告内容：

We introduce two formal methods of verifying quantum communication protocols. One is to take advantage of quantum process algebras and the other is to make use of theorem provers. With a suitable notion of behavioural equivalence and a decision method, we can determine if an implementation of a protocol is consistent with its specification. Ground bisimulation is a convenient behavioural equivalence for quantum processes because of its associated coinduction proof technique. We exploit this technique to design and implement two on-the-fly algorithms for the strong and weak versions of ground bisimulation to check if two given processes in quantum CCS are equivalent. We have developed a tool that can verify interesting quantum protocols such as the BB84 quantum key distribution scheme. At a low level, quantum protocols can be implemented by quantum circuits. We propose a symbolic approach to reasoning about the functional correctness of quantum circuits. It is based on a small set of laws involving some basic manipulations on vectors and matrices. This symbolic reasoning scales well and is suited to be automated in Coq, as demonstrated with some typical examples.

报告人简介：

邓玉欣，华东师范大学教授，软件工程学院副院长，上海市计算机学会理论专委会主任。主要研究方向包括并发计算模型、程序理论、量子计算，代表性工作包括一个已经被国外学者写进教科书的“邓引理”(Deng Lemma)和关于概率并发理论的一部英文专著。发表学术论文85篇，多篇出现在国际权威期刊和会议如Information and Computation、Theoretical Computer Science、ICALP、LICS、POPL等。曾为CONCUR 2018作特邀报告。在近40次国际会议中任程序委员会委员，其中包括CAV 2021、CAV 2022、LICS 2023等。