Verification and Analysis of Quantum Programs
Funding: 2018: $131,300
2019: $124,000
2020: $129,510
Project Member(s): Feng, Y., Ying, M.
Funding or Partner Organisation: Australian Research Council (ARC Discovery Projects)
Australian Research Council (ARC Discovery Projects)
Start year: 2018
Summary: Verification and analysis of quantum programs. This project aims to develop theoretical foundations and techniques, as well as efficient algorithms and effective tools, for the verification and analysis of quantum programs. This project will introduce new ideas and techniques to tackle the problem of verifying and analysing quantum programs and provide efficient algorithms and effective tools to help quantum program compilation and optimisation. Successful development of the outcomes and tools in this project will help Australian industries build frontier technologies for quantum software engineering and establish and preserve their competitive status in the era of quantum computing.
Publications:
Barthe, G, Hsu, J, Ying, M, Yu, N & Zhou, L 2020, 'Relational proofs for quantum programs.', Proc. ACM Program. Lang., vol. 4, no. POPL, pp. 21:1-21:1.
View/Download from: Publisher's site
Guan, J, Feng, Y, Turrini, A & Ying, M 2019, 'Model Checking Applied to Quantum Physics.', CoRR, vol. abs/1902.03218.
Li, G, Zhou, L, Yu, N, Ding, Y, Ying, M & Xie, Y 2019, 'Poq: Projection-based Runtime Assertions for Debugging on a Quantum Computer.', CoRR, vol. abs/1911.12855.
Liu, J, Zhou, L & Ying, M 2019, 'Expected Runtime of Quantum Programs.', CoRR, vol. abs/1911.12557.
Wang, Q, Liu, J & Ying, M 2019, 'Equivalence Checking of Quantum Finite-State Machines.', CoRR, vol. abs/1901.02173, pp. 1-21.
View/Download from: Publisher's site
Ying, M 2019, 'Toward automatic verification of quantum programs.', Formal Aspects Comput., vol. 31, pp. 3-25.
View/Download from: Publisher's site
Liu, J, Zhan, B, Wang, S, Ying, S, Liu, T, Li, Y, Ying, M & Zhan, N 1970, 'Quantum Hoare Logic.', Arch. Formal Proofs.
Barthe, G, Hsu, J, Ying, M, Yu, N & Zhou, L 2019, 'Coupling Techniques for Reasoning about Quantum Programs.'.
Guan, J, Feng, Y & Ying, M 2018, 'Super-activating quantum memory with entanglement.', Quantum Inf. Comput., vol. 18, no. 13&14, pp. 1115-1124.
View/Download from: Publisher's site
Li, Y & Ying, M 2018, 'Algorithmic analysis of termination problems for quantum programs.', Proc. ACM Program. Lang., vol. 2, pp. 35:1-35:1.
View/Download from: Publisher's site
Ying, M & Feng, Y 2018, 'Model Checking Quantum Systems - A Survey.', CoRR, vol. abs/1807.09466, no. 1, pp. 28-31.
View/Download from: Publisher's site
Zhou, L, Ying, S, Yu, N & Ying, M 2018, 'Quantum Coupling and Strassen Theorem.', CoRR, vol. abs/1803.10393.
Hung, S-H, Hietala, K, Zhu, S, Ying, M, Hicks, M & Wu, X 2018, 'Quantitative Robustness Analysis of Quantum Programs (Extended Version).', CoRR.
Wang, Q & Ying, M 2018, 'Quantum Büchi Automata.', CoRR.
Ying, M & Li, Y 2018, 'Reasoning about Parallel Quantum Programs.'.
Ying, S & Ying, M 2018, 'Reachability analysis of quantum Markov decision processes.', pp. 31-51.
View/Download from: Publisher's site
Ying, S, Ying, M & Feng, Y 2017, 'Quantum Privacy-Preserving Data Analytics.'.
Ying, S, Ying, M & Feng, Y 2017, 'Quantum Privacy-Preserving Perceptron.'.
Guan, J, Feng, Y & Ying, M 2016, 'Decomposition of Quantum Markov Chains and Its Applications', Journal of Computer and System Sciences, vol. 95, pp. 55-68.
View/Download from: Publisher's site
Feng, Y & Ying, M 1970, 'Toward Automatic Verification of Quantum Cryptographic Protocols.', CONCUR, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, pp. 441-455.
FOR Codes: Expanding Knowledge in the Information and Computing Sciences, Computational Logic and Formal Languages