News

13.12.2024 Work on "A Practical Quantum Hoare Logic with Classical Variables, I" is online.

26.11.2024 ARC Discovery Project Awarded ($510,636)

Foundation of Refinement Techniques for Quantum Programming.

27.07.2023 

Work on "Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs"  is accepted for publication by Information & Computation

21.07.2023 

Work on "Single-Qubit Gates Matter for Optimising Quantum Circuit Depth in Qubit Mapping"  is accepted into ICCAD 2023.  

31.01.2023 

Work on "Verification of Nondeterministic Quantum Programs" by Yuan and Yingte has been accepted for presentation at ASPLOS23

19.11.2022 

Work on "Alternating Layered Variational Quantum Circuits Can Be Classically Optimized Efficiently Using Classical Shadows" has been accepted for presentation at AAAI-23 (https://arxiv.org/abs/2208.11623) 

14.07.2022

Work on "Equivalence Checking of Dynamic Quantum Circuits"  (https://arxiv.org/abs/2106.01658) is accepted into ICCAD 2022.  

 Work on "Abstract interpretation, Hoare logic, and incorrectness logic for quantum programs"  (https://arxiv.org/abs/2206.13772) is online.

 Work on "Supervised Learning Enhanced Quantum Circuit Transformation"  (https://arxiv.org/abs/2110.03057) is accepted for publication by IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems (TCAD).  

Our work on "Verification of Distributed Quantum Programs"  (https://arxiv.org/abs/2104.14796) is accepted for publication by ACM Transactions on Computational Logic.

The TDD work (https://arxiv.org/abs/2009.02618) is accepted for publication by ACM Transactions on Design Automation of Electronic Systems, a premier ACM journal in design and automation of electronic systems.

A significant extension of our MCTS work (presented at ICCAD-20, https://arxiv.org/abs/2008.09331) is accepted for publication by ACM Transactions on Design Automation of Electronic Systems, a premier ACM journal in design and automation of electronic systems.

ARC Discovery Project Awarded (DP220102059, $435,000.00, University of Technology Sydney 0802)

Professor Mingsheng Ying; Professor Yuan Feng; Professor Sanjiang Li; Assistant Professor Robert 

Rand

Formal Verification of Quantum Logic Circuits. 

Abstract: 

The project aims to develop comprehensive theory and effective techniques for formal modelling, equivalence checking, and model checking of quantum circuits. The research is timely as the rapid growth of quantum computing hardware makes it an urgent task to develop verification techniques for quantum hardware design and quantum compilers. The successful development of the algorithms and software tools proposed in this project will significantly advance the knowledge on formal verification of quantum circuits and help Australian quantum start-ups build and maintain an internationally leading position in the rapidly emerging quantum electronic design automation (EDA) industry.

 A new work entitled "Equivalence Checking of Dynamic Quantum Circuits" is available at arXiv: 2106.01658. 

A new work entitled "Verification of Distributed Quantum Programs" is available at arxiv:2104.14796. 

Our paper entitled "Approximate Equivalence Checking of Noisy Quantum Circuits" was accepted to DAC'21, the premier conference devoted to the design & automation of electronic systems (EDA). 

veriQC.com domain registration with GoDaddy! 

The book entitled "Model Checking Quantum Systems: Principles and Algorithms"  by Mingsheng and Yuan was published by Cambridge University Press.