|Institutional Office Address
DMIF, Room NN1, Phone: +39 0432 558440
|Research Project Title
Model Checking of Quantum Algorithms and Protocols
|Research Project Description
The aim of this project is to provide languages and tools for the design, implementation, simulation and formal verification of quantum algorithms and protocols.
Our main goal is to allow an high-level way of thinking about quantum computation and quantum information. In the context of quantum computation, which is based on the counter-intuitive laws of quantum physics, the possibility of testing quantum protocols is very important. In particular protocols for quantum key distribution (QKD) which are already used (for now in experimental settings) by banks for the secure transmission of information and must be correct and avoid errors.
We have implemented a framework -called Entangle- which provides a translation from a quantum programming language (Quipper) to a quantum model checking language (QPMC) and we are investigating quantum properties of entanglement-based QKD protocols.
In particular, we are interested in the investigation of spatial (if any) and temporal properties of quantum protocols and in the automated detection of decoherence using model checking techniques.