×

Toward automatic verification of quantum programs. (English) Zbl 1425.68271


MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68Q12 Quantum algorithms and complexity in the theory of computing
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Altenkirch T, Grattage J (2005) A functional quantum programming language. In: Proceedings of the 20th IEEE symposium on logic in computer science (LICS), pp 249-258
[2] Ambainis A, Bach E, Nayak A, Vishwanath A, Watrous J (2001) One-dimensional quantum walks. In: Proceedings of the 33rd ACM symposium on theory of computing (STOC), pp 37-49 · Zbl 1323.81021
[3] Apt, K.R., de Boer, F.S., Olderog, E.-R.: Verification of sequential and concurrent programs. Springer, London (2009) · Zbl 1183.68361 · doi:10.1007/978-1-84882-745-5
[4] Ardeshir-Larijani E, Gay SJ, Nagarajan R (2014) Verification of concurrent quantum protocols by equivalence checking. In: Proceedings of the 20th international conference on tools and algorithms for the construction and analysis of systems (TACAS), pp 500-514
[5] Baltag, A., Smets, S.: LQP: the dynamic logic of quantum information. Math Struct Comput Sci 16, 491-525 (2006) · Zbl 1103.03031 · doi:10.1017/S0960129506005299
[6] Barthe G, Fournet C, Grégoire B, Strub P-Y, Swamy N, Zanella Béguelin S (2014) Probabilistic relational verification for cryptographic implementations. In: Proceedings of the 41st annual ACM symposium on principles of programming languages (POPL), pp 193-206 · Zbl 1284.68380
[7] Barthe G, Köpf B, Olmedo F, Zanella Béguelin Z (2013) Probabilistic relational reasoning for differential privacy. In: ACM transactions on programming languages and systems, vol 35, No. 9 · Zbl 1321.68182
[8] Brunet, O., Jorrand, P.: Dynamic quantum logic for quantum programs. Int J Quantum Inf 2, 45-54 (2004) · Zbl 1069.81007 · doi:10.1142/S0219749904000067
[9] Chadha, R., Mateus, P., Sernadas, A.: Reasoning about imperative quantum programs. Electron Notes Theor Comput Sci 158, 19-39 (2006) · Zbl 1273.03104 · doi:10.1016/j.entcs.2006.04.003
[10] Chakarov A, Sankaranarayanan S (2013) Probabilistic program analysis with martingales. In: Proceedings of the 25th international conference on computer aided verification (CAV). Springer LNCS 8044, pp 511-526
[11] Chatterjee K, Fu HF, Novotný P, Hasheminezhad R (2016) Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. In: Proceedings of the 43rd annual ACM symposium on principles of programming languages (POPL), pp 327-342 · Zbl 1347.68075
[12] Cleve, R., Buhrman, H.: Substituting quantum entanglement for communication. Phys Rev A 56, 1201-1204 (1997) · doi:10.1103/PhysRevA.56.1201
[13] Colón MA, Sankaranarayanan S, Sipma HB (2003) Linear invariant generation using non-linear constraint solving. In: Proceedings of the 15th international conference on computer aided verification (CAV). Springer LNCS, pp 420-433 · Zbl 1278.68164
[14] Dale, H., Jennings, D., Rudolph, T.: Provable quantum advantage in randomness processing. Nat Commun 6, 8203 (2015) · doi:10.1038/ncomms9203
[15] D’Hondt, E., Panangaden, P.: Quantum weakest preconditions. Math Struct Comput Sci 16, 429-451 (2006) · Zbl 1122.68058 · doi:10.1017/S0960129506005251
[16] Feng, Y., Duan, R.Y., Ji, Z.F., Ying, M.S.: Proof rules for the correctness of quantum programs. Theor Comput Sci 386, 151-166 (2007) · Zbl 1137.68038 · doi:10.1016/j.tcs.2007.06.011
[17] Feng Y, Hahn EM, Turrini A, Zhang LJ (2015) QPMC: a model checker for quantum programs and protocols. In: Proceedings of the 20th international symposium on formal methods (FM). Springer LNCS 9109, pp 265-272
[18] Feng Y, Ying MS (2015) Toward automatic verification of quantum cryptographic protocols. In: Proceedings of the 26th international conference on concurrency theory (CONCUR), pp 441-455 · Zbl 1374.68327
[19] Feng, Y., Yu, N.K., Ying, M.S.: Model checking quantum Markov chains. J Comput Syst Sci 79, 1181-1198 (2013) · Zbl 1311.68086 · doi:10.1016/j.jcss.2013.04.002
[20] Fioriti LMF, Hermanns H (2015) Probabilistic termination: soundness, completeness, and compositionality. In: Proceedings of the 42nd annual ACM symposium on principles of programming languages (POPL), pp 489-501 · Zbl 1345.68104
[21] Gay SJ, Papanikolaou N, Nagarajan R (2008) QMC: a model checker for quantum systems. In: Proceedings of the 20th international conference on computer aided verification (CAV). Springer LNCS 5123, pp 543-547
[22] Gleason, A.M.: Measures on the closed subspaces of a Hilbert space. J Math Mech 6, 885-893 (1957) · Zbl 0078.28803
[23] Gorelick GA (1975) A complete axiomatic system for proving assertions about recursive and non-recursive programs. Technical Report, Department of Computer Science, University of Toronto
[24] Green A, Lumsdaine PL, Ross NJ, Selinger P, Valiron B (2013) Quipper: a scalable quantum programming language. In: Proceedings of the 34th ACM conference on programming language design and implementation (PLDI), pp 333-342 · Zbl 1406.68013
[25] Grover LK (1997) Quantum telecomputation. arXiv:quant-ph/9704012
[26] Harel D (1979) First-order dynamic logic, LNCS 68. Springer · Zbl 0403.03024
[27] Den Hartog, J., de Vink, E.P.: Verifying probabilistic programs using a Hoare like logic. Int J Found Comput Sci 13, 315-340 (2002) · Zbl 1066.68081 · doi:10.1142/S012905410200114X
[28] Leymann, T.: Hoare logic and auxiliary variables. Formal Asp Comput 11, 541-566 (1999) · Zbl 0978.03026 · doi:10.1007/s001650050057
[29] Katoen J-P, McIver A, Meinicke L, Morgan CC (2010) Linear-invariant generation for probabilistic programs—automated support for proof-based methods. In: Proceedings 17th international symposium on static analysis (SAS). Springer LNCS 6337, pp 390-406 · Zbl 1239.68020
[30] Kubota, T., Kakutani, Y., Kato, G., Kawano, Y., Sakurada, H.: Semi-automated verification of security proofs of quantum cryptographic protocols. J Symb Comput 73, 192-220 (2016) · Zbl 1336.68164 · doi:10.1016/j.jsc.2015.05.001
[31] JavadiAbhari, A., Patil, S., Kudrow, D., Heckey, J., Lvov, A., Chong, F.T., Martonosi, M.: ScaffCC: scalable compilation and analysis of quantum programs. Parallel Comput 45, 2-17 (2015) · doi:10.1016/j.parco.2014.12.001
[32] Kakutani Y (2009) A logic for formal verification of quantum programs. In: Proceedings of the 13th Asian computing science conference (ASIAN 2009). Springer LNCS 5913, pp 79-93 · Zbl 1273.03107
[33] Li YJ, Ying MS (2018) Algorithmic analysis of termination problems for quantum programs. In: Proceedings of the 45th annual ACM symposium on principles of programming languages (POPL), pp 35.1-35.29
[34] Li, Y.J., Yu, N.K., Ying, M.S.: Termination of nondeterministic quantum programs. Acta Inf 51, 1-24 (2014) · Zbl 1359.68092 · doi:10.1007/s00236-013-0185-3
[35] Liu T, Li YJ, Wang SL, et al A theorem prover for quantum Hoare logic and its applications. arXiv:1601.03835
[36] Mateus, P., Sernadas, A.: Weakly complete axiomatization of exogenous quantum propositional logic. Inf Comput 204, 771-794 (2006) · Zbl 1116.03021 · doi:10.1016/j.ic.2006.02.001
[37] van Meter R, Munro WJ, Nemoto K, Itoh KM (2008) Arithmetic on a distributed-memory quantum multicomputer. ACM J Emerg Technol Comput Syst 3, Art. No. 17
[38] McIver, A., Morgan, C.: Abstraction, refinement and proof for probabilistic systems. Springer, Berlin (2005) · Zbl 1069.68039
[39] Nielsen, M.A., Chuang, I.L.: Quantum computation and quantum information. Cambridge University Press, Cambridge (2000) · Zbl 1049.81015
[40] Paykin J, Rand R, Zdancewic S (2017) QWIRE: a core language for quantum circuits. In: Proceedings of the 44th annual ACM symposium on principles of programming languages (POPL), pp 846-858 · Zbl 1380.68087
[41] Rand R Verification logics for quantum programs. http://www.cis.upenn.edu/ rrand/wpe.pdf
[42] Sankaranarayanan S, Sipma HB, Manna Z (2004) Non-linear loop invariant generation using Gröbner bases. In: Proceedings of the 31st ACM symposium on principles of programming languages (POPL), pp 318-329 · Zbl 1325.68071
[43] Selinger, P.: Towards a quantum programming language. Math Struct Comput Sci 14, 527-586 (2004) · Zbl 1085.68014 · doi:10.1017/S0960129504004256
[44] Serafini A, Mancinians S, Bose S (2006) Distributed quantum computation via optical fibers. Phys Rev Lett 96, Art. No. 010503
[45] Svore K, Geller A, Troyer M, Azariah J, Granade C, Heim B, Kliuchnikov V, Mykhailova M, Paz A, Roetteler M (2018) Q#: enabling scalable quantum computing and development with a high-level DSL. In: Proceedings of the real world domain specific languages workshop 2018, Art. no. 8
[46] Tani S, Kobayashi H, Matsumoto K (2012) Exact quantum algorithms for the leader election problem. ACM Trans Comput Theory 4, Art. No. 1 · Zbl 1322.68077
[47] Temme, K., Osborne, T.J., Vollbrecht, K.G., Poulin, D., Verstraete, F.: Quantum metropolis sampling. Nature 471, 87-90 (2011) · doi:10.1038/nature09770
[48] Unruh D Quantum relational Hoare logic. https://arxiv.org/pdf/1802.03188.pdf
[49] Wecker D, Svore KM (2014) LIQUi|>: a software design architecture and domain-specific language for quantum computing. arXiv:1402.4467
[50] Ying MS (2011) Floyd-Hoare logic for quantum programs. ACM Trans Program Lang Syst 39, Art. no. 19
[51] Ying MS (2016) Foundations of quantum programs. Morgan-Kaufmann
[52] Ying MS (2016) Toward automatic verification of quantum programs (extended abstract). In: Proceedings of the 2nd international symposium on dependable software engineering: theories, tools, and applications (SETTA)
[53] Ying, M.S., Chen, J.X., Feng, Y., Duan, R.Y.: Commutativity of quantum weakest preconditions. Inf Process Lett 104, 152-158 (2007) · Zbl 1184.68258 · doi:10.1016/j.ipl.2007.06.003
[54] Ying, MS; Feng, Y., No article title, Quantum loop programs. Acta Inf, 47, 221-250 (2010)
[55] Ying, M.S., Feng, Y.: A flow-chart language for quantum programming. IEEE Trans Softw Eng 37, 466-485 (2011) · doi:10.1109/TSE.2010.94
[56] Ying MS, Li YJ, Yu NK, Feng Y (2014) Model-checking linear-time properties of quantum systems. ACM Trans Comput Logic 15, Art. no. 22 · Zbl 1354.68090
[57] Ying MS, Ying SG, Wu XD (2017) Invariants of quantum programs: characterisations and generation. In: Proceedings of the 44th annual ACM symposium on principles of programming languages (POPL), pp 818-832 · Zbl 1380.68135
[58] Ying, M.S., Yu, N.K., Feng, Y., Duan, R.Y.: Verification of quantum programs. Sci Comput Program 78, 1679-1700 (2013) · doi:10.1016/j.scico.2013.03.016
[59] Ying SG, Feng Y, Yu NK, Ying MS (2013) Reachability analysis of quantum Markov chains. In: Proceedings of the 24th Int Conf Concurr Theory (CONCUR), pp 334-348 · Zbl 1390.68444
[60] Yu NK, Ying MS (2012) Reachability and termination analysis of concurrent quantum programs. In: Proceedings of the 23th international conference on concurrency theory (CONCUR), pp 69-83 · Zbl 1364.68145
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.