Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Lecture notes in computer science

Techniques for Formal Modelling and Analysis of Quantum Systems

Simon J. Gay, Rajagopal Nagarajan

Published Jan 1, 2013• 2 citations
Publisher
DOI
10.1007/978-3-642-38164-5_18

Related papers

The Simulation of Quantum Systems

David M. Ceperley

Recent Progress in Many-Body Theories•Jan 1, 1995•3 citations

Formal Analysis of Quantum Systems using Process Calculus

Timothy A. S. Davidson, Simon J. Gay, Rajagopal Nagarajan

Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods, such as formal logics for specification, formal modelling languages, separation of levels of abstraction, and compositional analysis. We argue that these techniques will be necessary for the analysis of large-scale systems that combine quantum and classical components, and summarize the results of initial investigation using behavioural equivalence in process calculus. This paper is a summary of Simon Gay's invited talk at ICE'11.

arXiv:1108.0469•Electronic Proceedings in Theoretical Computer Science•Jul 31, 2011•6 citations

Formal Analysis of Quantum Optics

Mohamed Yousri Mahmoud

At the beginning of the last century, the theory of quantum optics arose and led to a revolution in physics, since it allowed the interpretation of many unknown phenomena and the development of numerous powerful, cutting edge engineering applications, \nsuch as high precision laser technology. The analysis and verification of such applications and systems, however, are very complicated. Moreover, traditional analysis tools, e.g., simulation, numerical methods, computer algebra systems, and paper-and-pencil approaches are not well suited for quantum systems. In the last decade, a new emerging verification technique, called formal methods, became common among engineering domains, and has proven to be effective as an analysis tool. Formal methods \nconsist in the development of mathematical models of the system subject for analysis, and deriving computer-aided mathematical proofs. In this thesis, we propose a framework for the analysis of quantum optics based on formal methods, in particular theorem proving. The framework aims at implementing necessary quantum mechanics and optics concepts and theorems that facilitate the modelling of quantum optical devices and circuits, and then reason about them formally. To this end, the framework \nconsists of three major libraries: 1) Mathematical foundations, which mainly contain the theory of complex-valued-function linear spaces, 2) Quantum mechanics, which develops the general rules of quantum physics, and 3) Quantum Optics, which \nspecializes these rules for light beams and implements all related concepts, e.g., light coherence which is typically emitted by laser sources. On top of these theoretical foundations, we build a library of formal models of a number of optical devices commonly \nused in quantum circuits, including, beam splitters, light displacers, and light phase shifters. Using the proposed framework, we have been able to formally verify common quantum optical computing circuits, namely the Flip gate, CNOT gate, and Mach-Zehnder interferometer.

•Sep 1, 2015•3 citations

Methodology of Analytic and Computational Studies on Quantum Systems

Masuo Suzuki

Journal of Statistical Physics•Mar 1, 2003•8 citations

Formal Verification of Quantum Protocols

Rajagopal Nagarajan, Gay, Simon

We propose to analyse quantum protocols by applying formal verification techniques developed in classical computing for the analysis of communicating concurrent systems. One area of successful application of these techniques is that of classical security protocols, exemplified by Lowe's discovery and fix of a flaw in the well-known Needham-Schroeder authentication protocol. Secure quantum cryptographic protocols are also notoriously difficult to design. Quantum cryptography is therefore an interesting target for formal verification, and provides our first example; we expect the approach to be transferable to more general quantum information processing scenarios. The example we use is the quantum key distribution protocol proposed by Bennett and Brassard, commonly referred to as BB84. We present a model of the protocol in the process calculus CCS and the results of some initial analyses using the Concurrency Workbench of the New Century (CWB-NC).

arXiv:quant-ph/0203086•Mar 18, 2002•24 citations

A Symbolic Approach to Verifying Quantum Systems

Parosh Aziz Abdulla

A Symbolic

Communications of the ACM•May 29, 2025•2 citations
Quantum communication and cryptographic protocols are well on the way to becoming an important practical technology. Although a large amount of successful research has been done on proving their correctness, most of this work does not make use of familiar techniques from formal methods, such as formal logics for specification, formal modelling languages, separation of levels of abstraction, and compositional analysis. We argue that these techniques will be necessary for the analysis of large-scale systems that combine quantum and classical components, and summarize the results of initial investigation using behavioural equivalence in process calculus. This paper is a summary of Simon Gay's invited talk at ICE'11.
At the beginning of the last century, the theory of quantum optics arose and led to a revolution in physics, since it allowed the interpretation of many unknown phenomena and the development of numerous powerful, cutting edge engineering applications, \nsuch as high precision laser technology. The analysis and verification of such applications and systems, however, are very complicated. Moreover, traditional analysis tools, e.g., simulation, numerical methods, computer algebra systems, and paper-and-pencil approaches are not well suited for quantum systems. In the last decade, a new emerging verification technique, called formal methods, became common among engineering domains, and has proven to be effective as an analysis tool. Formal methods \nconsist in the development of mathematical models of the system subject for analysis, and deriving computer-aided mathematical proofs. In this thesis, we propose a framework for the analysis of quantum optics based on formal methods, in particular theorem proving. The framework aims at implementing necessary quantum mechanics and optics concepts and theorems that facilitate the modelling of quantum optical devices and circuits, and then reason about them formally. To this end, the framework \nconsists of three major libraries: 1) Mathematical foundations, which mainly contain the theory of complex-valued-function linear spaces, 2) Quantum mechanics, which develops the general rules of quantum physics, and 3) Quantum Optics, which \nspecializes these rules for light beams and implements all related concepts, e.g., light coherence which is typically emitted by laser sources. On top of these theoretical foundations, we build a library of formal models of a number of optical devices commonly \nused in quantum circuits, including, beam splitters, light displacers, and light phase shifters. Using the proposed framework, we have been able to formally verify common quantum optical computing circuits, namely the Flip gate, CNOT gate, and Mach-Zehnder interferometer.
We propose to analyse quantum protocols by applying formal verification techniques developed in classical computing for the analysis of communicating concurrent systems. One area of successful application of these techniques is that of classical security protocols, exemplified by Lowe's discovery and fix of a flaw in the well-known Needham-Schroeder authentication protocol. Secure quantum cryptographic protocols are also notoriously difficult to design. Quantum cryptography is therefore an interesting target for formal verification, and provides our first example; we expect the approach to be transferable to more general quantum information processing scenarios. The example we use is the quantum key distribution protocol proposed by Bennett and Brassard, commonly referred to as BB84. We present a model of the protocol in the process calculus CCS and the results of some initial analyses using the Concurrency Workbench of the New Century (CWB-NC).