Abstract
The characteristic difficulty in creating pure quantum software is mainly due to the inaccessibility to intermediate states, which makes debugging practically impossible. However, the use of formal methods, which apply rigorous mathematical models to ensure error-free software, can overcome this barrier and enable the production of reliable quantum algorithms and applications right out of the box.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Cartiere CR (2020) Formal quantum software engineering: introducing the formal methods of software engineering to quantum computing. https://doi.org/10.13140/RG.2.2.26157.10725/2
Woodcock J, Davies J (1996) Using Z. Specification, refinement, and proof. Prentice Hall
Cartiere CR (2013) Quantum software engineering: bringing the classical software engineering into the quantum domain. Master’s Thesis, University of Oxford, Department of Computer Science, Software Engineering Programme
Jacky J (1996) The way of Z: practical programming with formal methods. Cambridge University Press
Ruhela V (2012) Z formal specification language – an overview. Int J Eng Res Technol (IJERT) 01(06)
Dirac P (1958) The principles of quantum mechanics, 4th edn. Oxford University Press
Mateus P, Sernadas A (2004) Reasoning about quantum systems. In: Alferes JJ, Leite J (eds) Logics in artificial intelligence. JELIA 2004. Lecture Notes in Computer Science, vol 3229. Springer, Berlin
Barenco A (1998) Quantum computation: an introduction. In: Lo H, Popescu S, Spiller T (eds) Introduction to quantum computation and information. World Scientific
Feynman R (1982) Simulating physics with computers. Int J Theor Phys 21:467–488
Deutsch D (1985) Quantum theory, the church-turing principle and the universal quantum computer. Proc R Soc Lond A 400:97–117
Green AS. The QIO package. Haskell community’s central package archive of open source soft. https://hackage.haskell.org/package/QIO, v1.3
Bennett CH, Brassard G, Crépeau C, Jozsa R, Peres A, Wootters WK (1993) Teleporting an unknown quantum state via dual classical and Einstein-Podolsky-Rosen channels. Phys Rev Lett 70:1895
Nielsen M, Chuang I (2010) Quantum computation and quantum information: 10th Anniversary Edition. Cambridge University Press, Cambridge. https://doi.org/10.1017/CBO9780511976667
Greenwood GW (2001) Finding solutions to NP problems: philosophical difference between quantum and evolutionary search algorithms. Portland State University, Portland, OR
Gross AM, Stallard J (2007) Implementing Grover’s algorithm using linear transformations in Haskell. In: Proceedings of the Eighth Symposium on Trends in Functional Programming, vol 8. p XXV
Deutsch D, Jozsa R (1992) Rapid solutions of problems by quantum computation. Proc R Soc Lond A 439:553
Simon DR (1997) On the power of quantum computation. SIAM J Comput 26(5):1474–1483
Kaye P, Laflamme R, Mosca M (2007) An introduction to quantum computing. Oxford University Press
Spivey JM (1992) The Z notation: a reference manual. Prentice Hall International
Saaltink M (1993) Z and EVES. Technical Report TR-91-5449-02
Roberts D, Nelms J, Starkey D, Thomas S (2012) Travelling by teleportation. Phys Spl Top J. University of Leicester
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this chapter
Cite this chapter
Cartiere, C.R. (2022). Formal Methods for Quantum Software Engineering. In: Serrano, M.A., Pérez-Castillo, R., Piattini, M. (eds) Quantum Software Engineering. Springer, Cham. https://doi.org/10.1007/978-3-031-05324-5_5
Download citation
DOI: https://doi.org/10.1007/978-3-031-05324-5_5
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-05323-8
Online ISBN: 978-3-031-05324-5
eBook Packages: Computer ScienceComputer Science (R0)