Formal Verification of Quantum Programs

2024年11月12日(周二) 10: 00~11:00

信管学院308会议室

Yuxin Deng(邓玉欣) received his BEng (1999) and MSc (2002) from Shanghai Jiao Tong University, China, and PhD (2005) from Ecole des Mines de Paris, France. He was a research associate at University of New South Wales, Australia (2005-2006), an associate Professor at Shanghai Jiao Tong University, China (2006-2015), a visiting research fellow at Carnegie Mellon University, USA (2011), and a seconded expert at UNESCO Headquarters, France (2012-2014). In 2015 he joined East China Normal University as a full Professor. His research interests include concurrency theory, especially about process calculi, and formal semantics of programming languages, as well as quantum computing. He authored a monograph on the semantics of probabilistic processes and a textbook on functional programming. He was a keynote speaker of CONCUR 2018. He is a CCF distinguished member and a recipient of the second prize in natural science of the 2024 CCF science and technology achievement award.

Formal Verification of Quantum Programs

In this talk we introduce three formal methods for quantum program verification: bisimulation checking, theorem proving, and Hoare logic. Firstly, we use ground bisimulation to describe the behavioral equivalence of quantum CCS processes and develop a tool to verify the functional correctness of quantum communication protocols. Secondly, we propose a symbolic reasoning method for proving the correctness of quantum circuits. It is based on a set of fundamental laws of vectors and matrices, and is suitable for automation in theorem provers like Coq. Finally, we propose a new quantum Hoare logic that employs distribution formulas to describe probabilistic properties, facilitating local reasoning of probabilistic behavior and verifying the correctness of typical quantum algorithms such as HHL and Shor’s algorithm.