Qbricks

An automated deductive verification framework for circuit-building quantum programs

drawing

Welcome to Qbricks

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.

Soon available code

Due to some policy adjustments from our host institution, we are currently unable to provide Qbricks code, this will be fixed in a near future.

open_positions

PhD open positions (3 years): Probing quantum verification in the NISQ era

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

PostDoc open position (2 years) : verified compilation

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

How to apply

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

News

People

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

Publications

International conference

Survey

Preprint

Short articles