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 doctoral position is to probe formal verification against first generation of quantum application (NISQ era). Possibilities include, among other: extending Qbricks semantic and proof model to the hybrid paradigm, develop and implement a specification and proof system for error propagation and correction in quantum computing, develop certified ready-to-use NISQ applications.
Keywords: quantum programming, formal verification, NISQ, quantum error correction
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 sebastien.bardin@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: Sébastien Bardin (CEA), Christophe Chareton (CEA) Contact: sebastien.bardin@cea.fr
- 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 |
- An Automated Deductive Verification Framework for Circuit-building Quantum Programs, March, 2021 at ESOP’21.
- 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)