PhD Defense
Jérome Ricciardi
Title: Practical Verification of Quantum Circuit Transformations
Date: Thursday, 4 June 2026
Time: 14:00, Paris time (CEST)
Legal status: Public PhD defense
Language: English
Format: 45-minute presentation, followed by questions
Location: École normale supérieure Paris-Saclay, room 1Z61
Address: 4 avenue des Sciences, 91190 Gif-sur-Yvette, France
Registration
For organisational reasons, ENS needs the list of participants attending the defence. Registration also helps me estimate how many people will attend the drinks and snacks after the defence.
Defense video link: TODO public videoconference link
Jury video link: TODO private videoconference link for jury members
Institutional Framework
- Degree-awarding institution: Université Paris-Saclay
- Doctoral school: STIC - Sciences and Technologies of Information and Communication
- Research units: LMF and LSL
- Thesis supervisor: Benoît Valiron, LMF
- CEA advisor: Christophe Chareton, CEA-List
Abstract
Quantum computing, based on the principles of quantum physics, promises significant gains in computational power. However, it introduces new challenges, particularly for program verification. Classical verification techniques do not apply directly to quantum computing. This is mainly due to the use of quantum memory (non-standard information unit) and its measurement operation, which is the only way to retrieve information from a quantum bit and introduces a probabilistic aspect.
In this thesis, we focus on the circuit-based quantum computing model and a practical aspect of it: circuit transformations. A quantum circuit can be purely quantum (unitary circuit) or include classical control and measurement (hybrid circuit). Circuit transformations occur throughout the quantum computation process, whether compiling a circuit described in a high-level language to a low-level language, optimising a circuit for specific hardware (transpilation), changing the computation model, or transferring a quantum state (teleportation).
Each of these transformations can alter the circuit's behaviour. Therefore, tools are needed to verify that the behaviour is preserved. However, current tools are mostly limited to the unitary case, thus restricted to verifying transformations that do not change the type of circuit: a unitary circuit is transformed into a unitary circuit. Those that venture into the hybrid case are limited to hybridisation: a unitary circuit is transformed into a hybrid. The real challenge arises with the introduction of auxiliary wires, such as ancillas or discards for hybrid circuits, as it must be ensured that these auxiliary wires do not affect the others.
Several techniques exist for verifying a circuit (simulation, symbolic execution, proof), differing in their automation and scalability. Simulation, while automatable, lacks scalability. Symbolic execution, which can be automated, scales better. Proof, while scalable, is challenging to automate. We thus chose to use both proof and symbolic execution. We use proof to certify a compilation pass from a high-level language to a low-level language. We also use symbolic execution by developing a tool to verify the equivalence of hybrid circuits using discard.
To assist us in the proof process, we utilise the semi-automatic proof tool Qbricks, which is capable of proving parametrised unitary circuits based on path sums. This formalism allows for compact and encodable modelling of circuits.
As a prerequisite for developing our verification tool for hybrid circuits with discard, we define partial equivalence relations for unitary circuits and a mechanism to extend unitary verification tools to hybrid circuits. The combination of these two components enables the handling of hybrid circuits with discard.
To evaluate our approach, we implement in the tool SQbricks our equivalence relations and our mechanism for extending tools limited to unitary circuits. We have demonstrated that unitary tools extended to the hybrid case without discard vastly surpass the state of the art. Moreover, by adding a separation test at the unitary level, we can handle much larger classes.
Jury
- Miriam Backens - jury member, LORIA
- Sylvie Boldo - jury member, Inria
- Aleks Kissinger - reviewer, University of Oxford
- Alessandra Di Pierro - reviewer, University of Verona
Access
The defense will take place at École normale supérieure Paris-Saclay, room 1Z61, 4 avenue des Sciences, 91190 Gif-sur-Yvette.
From Paris, take RER B towards Saint-Rémy-lès-Chevreuse to Le Guichet, then bus 9108 or 4609 to Moulon. Alternatively, take RER B or RER C to Massy-Palaiseau, then bus 4606 or 91.06B to Moulon.
After the Defense
Drinks and snacks will be served after the defense in the billiards room of building 650. Open in Google Maps
Later in the evening, between 7pm and 8pm depending on when the defence finishes, we’ll be continuing at Hall Of Beer Open in Google Maps