Qbricks is open-source environment for automated formal verification of quantum programs. It enables the writing of quantum circuit building programs, specified with their I/O functions and/or their resource requirements. Thanks to a characterization of quantum circuits as paramatrized path-sums, the specifications of Qbricks circuit-building quantum programs reduces to first-order proof obligations. Its host language, the Why3 deductive verification environment, provides an interface with SMT-solvers, enabling an high-level of automation in the vertfication of Qbricks specifications.
So far, Qbricks framework enabled the verified implementation of several emblematic algorithm from the litterature, including the Deutsch-Jozsa algorithm, Quantum Phase Estimation (QPE), Grover search algorithm and Shor order finding (including an implementation of the oracle).
It is developed at the CEA LIST (part of Université Paris-Saclay) in collaboration with Laboratoire Méthodes Formelles(Université Paris-Saclay).
For an introduction to Qbricks, please read our article and see the related presentation slides. A tutorial redaction is under progress.
The goal of this post-doctoral position is to extend formal verification practice to quantum compilation. Possibilities include, among others, error correction mechanisms in certified quantum code, together with specifications and reasoning technique for certifying its reliability, automatized certified optimizer for quantum circuits, hardware agnostic assembly language together with its compiler,
Keywords: quantum programming, compilation, optimization, formal verification
Applications should be sent to christophe.chareton@cea.fr as soon as possible (first come, first served) and by early July 2021 at the latest. Candidates should send a CV, a cover letter, a transcript of all their university results, as well as contact information of two references. Each position is expected to start in October 2021.
Advisors: Christophe Chareton (CEA), Sébastien Bardin (CEA) Contact: christophe.chareton@cea.fr
- Our code is back to open source diffusion, under License LGPL, 2.1, April 2022 .
- Ongoing internship April 2022 Welcome, Mohamed Bassiouny, working on automated circuit equivalence verification.
- Book chapter submission March 2022 Our survey on formal methods in quantum computing was submitted, as a Book Chapter to appear in the " "Handbook of Formal Analysis and Verification in Cryptography" (CRC), see the preprint.
- Ongoing PhD March 2022 Welcome, Jérôme Ricciardi, working on mixed path-sums.
- Ongoing internship February 2022 Welcome, Tomas Barros Carneiro, working on an imperative developement interface for quantum formal verification.
- Presentation at IQFA Nov 2021 Qbricks was presented at the 12th Colloquium on Quantum Engineering, Fundamental Aspects to Applications, 2021 (slides).
- Online survey Formal Methods for Quantum Programs: A Survey September 2021.
- Presentation at QPL June 2021 Qbricks was presented at the 2021 online QPL conference (slides).
- Qbricks at ESOP March 2021 Glad to participate to the 2021 online ESOP conference (slides).
- Paper accepted December 2020 Proud that our paper “An Automated Deductive Verification Framework for Circuit-building Quantum Programs” has been accepted at ESOP’21.
- Online preprint March, 2020 Our preprint Toward certified quantum programming is availeble on Arxiv
- Talk at IWQC November, 2020, with online presentation
| Name | Position | Affiliation | Web site |
|---|---|---|---|
| Sébastien Bardin | Senior | CEA LIST, Université Paris-Saclay | Sébastien Bardin |
| Benoît Valiron | Senior | LMF, Université Paris-Saclay | Benoît Valiron |
| Christophe Chareton | Junior | CEA LIST, Université Paris-Saclay | Christophe Chareton |
| Jérôme Ricciardi | PhD student | CEA LIST, Université Paris-Saclay | Jérôme Ricciardi |
| Tomas Barros Carneiro | Intern | CEA LIST, Université Paris-Saclay | Tomas Barros Carneiro |
| Mohamed Bassiouny | Intern | CEA LIST, Université Paris-Saclay | Mohamed Bassiouny |
- An Automated Deductive Verification Framework for Circuit-building Quantum Programs, March, 2021 at ESOP’21.
- Formal Methods for Quantum Programs: A Survey, 09/2021. Due to the destructive aspect of quantum measurement, formal methods are prone to play a decisive role in the emerging field of quantum software. In this survey, we present the challenges adressed to formal verificatio at every stage of the quantum development process: high-level program design, implementation, compilation, etc. and we introduce the current most promising research directions
- Toward certified quantum programming, March, 2020
- A formally certified implementation of Shor algorithm quantum circuit, IWQC, November 2020 video
- Qbricks, a framework for formal verification in quantum computing PlanQC, January 2020 video
- Toward_certified_quantum_programming_ IWQC, November,2018 (2nd International Workshop on Quantum Compilation).(link)
Please note that all the following tools are external tools, please refer to their webpage for more information.
-
Build Docker image
make build -
Build container
make container -
Start container
make start
-
cd Case_studies -
make ide_shor