verification

An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits

We introduce a new paradigm for analysing and finding bugs in quantum circuits. In our approach, the problem is given by a ‍triple P C Q and the question is whether, given a set P of quantum states on the input of a circuit C, the set of quantum …

A Quantum Interpretation of Separating Conjunction for Local Reasoning of Quantum Programs Based on Separation Logic

It is well-known that quantum programs are not only complicated to design but also challenging to verify because the quantum states can have exponential size and require sophisticated mathematics to encode and manipulate. To tackle the state-space …

Quantum Programming Languages (Dagstuhl Seminar 18381)

This report documents the program and the outcomes of Dagstuhl Seminar 18381 "Quantum Programming Languages", which brought together researchers from quantum computing and classical programming languages.

Communicating Quantum Processes

We define a language CQP (Communicating Quantum Processes) for modelling systems which combine quantum and classical communication and computation. CQP combines the communication primitives of the pi-calculus with primitives for measurement and …