Towards the Formal Verification of Quantum Optical Systems
M. Yousri, Vincent Aravantinos, Sofiène Tahar · 2012
Nowadays, optics has several applications in many industries. Quantum optics in particular plays an important role, e.g., in information technology. The systems developed using quantum optics have several applications which can be critical (with respect to either safety or financial aspects). Their verification is thus an extremely important problem. This is done usually with paper-and-pencil analysis, simulation or computer algebra systems. However these techniques have some flaws that we propose to address using formal verification, and, more specifically, theorem proving. In this position paper, we sketch a formalization of quantum optics using a theorem prover and describe potential applications of these techniques. We focus in particular on the implementation of quantum bits (i.e., the first step towards a quantum computer) using coherent laser light.