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.
3 years Postdoc position, CEA Paris-Saclay, France
Formal verification for quantum programming
Keywords: quantum programming, theory of programming langages, formal methods
The CEA List, Software Security Lab (LSL), has several open internship positions in the area of formal verification for quantum programming , to begin as soon as possible at Paris-Saclay, France. The positions are 4-6 month long and can open the way to a doctoral work . They are articulated around the Qbricks tool, which aims at providing an automated solution for quantum programming formal verification.
Topic: Quantum Programming and formal verification
Host: Commissariat à l’Énergie Atomique, Software Security Laboratory
Place: Paris-Saclay, France
Team: Qbricks
Advisor(s): Christophe Chareton, Sébastien Bardin (first.name@cea.fr)
Context. Quantum hardware has made tremendous progress, and useful quantum machines are expected to become available in a near future. Hence, the need to design and implement adequate software tooling for the quantum case, as available in the classical computing case. Our long term goal is to design and develop formal techniques and tools enabling productive and certified quantum programming. Especially, we develop Qbricks [1,2], a proof of concept environment for formally verified quantum programming language.
Current topics. We consider the standard quantum hybrid model, where a classical program builds a quantum circuit and sends it to a quantum co-processor. In these positions, we are interested in verification mechanisms aiming at ensuring that a quantum program implementation indeed satisfies its intended behaviour. We propose the following topics:
• high-level automatic verification of quantum programs for implicit program properties,
• design of verification oriented hybrid quantum programming languages
• high-level functional reasoning for quantum programs,
• circuit-level automatic verification of quantum programs,
• verification of circuit transformation and compilation
More details on these possibilities topics will be happily provided! The list is not exhaustive, ask us if you have some project in mind.
These positions include theoretical research as well as prototyping and experimental evaluation.The results will be implemented and evaluated on QBricks, our young development and verification environment for quantum programs.
Host Institution. CEA is a leading institute in research in France and Europe. We are part of List, its 700 persons institute dedicated to digital systems. Within List, the quantum verification group is a young and emerging six person team, developping quantum static analysis/verified programming and debugguing solutions. CEA List is located in Campus Paris Saclay.
Requirements: We welcome curious and enthusiastic candidates with a solid background in Computer Science, both theoretical and practical, and a specialization in either formal methods or quantum computing (it is assumed that candidates will dedicate some of their time upgrading their skills).
Application: Applicants should send an e-mail to Christophe Chareton (christophe.chareton@cea.fr ), including CV and motivation letter.
Deadline: as soon as possible. Contact us for more information .
References
[1] Christophe Chareton and Sébastien Bardin and François Bobot and Valentin Perrelle and Benoît Valiron. An Automated Deductive Verification Framework for Circuit-building Quantum Programs Programming Languages and Systems - 30th European Symposium on Programming, ESOP 2021
[2] Christophe Chareton, Dongho Lee, Benoît Valiron, Renaud Vilmart, Sébastien Bardin, Zhaowei Xu: Formal Methods for Quantum Algorithms. Handb. Formal Anal. Verification Cryptogr. 2023: 319-422
[3] Matthew Amy: Towards Large-scale Functional Verification of Universal Quantum Circuits. QPL 2018: 1-21
[4] Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying CoqQ: Foundational Verification of Quantum Programs. POPL 2023
News
- Ongoing Postdoc October 2023 Welcome, Nicolas Nalpon, working on certified compilation.
- Ongoing PhD September 2023 Welcome, Tomas Barros, working on formal verification and high-level programming.
- Ongoing Postdoc June 2023 Welcome, Nicolas Blanco, working on parametrized path-sums rewriting.
- New relase March 2023 Qbricks_1 is online! Available on main branch in diffusion, under License LGPL, 2.1. As main novelties the release provides:
- LANGUAGE : new primitive constructs, containing (1) generic wiring and subcircuit control features (2) further gate constructors as primitives (Toffoli, Fredkin, X,Y,Z rotations, etc).
- COMPILATION : a fully formally verified circuit transformation process, targetting Oqasm compatibile circuit, and an oqasm output generating function. Works for circuit without ancilla qbits.
- CASE STUDIES : new implementations of Shor algorithm, illutrating imperative QBricks styled programmation and the Oqasm extraction functionality.- 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
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 |
| Nicolas Blanco | Postdoc | CEA LIST, Université Paris-Saclay | Nicolas Blanco |
| Nicolas Nalpon | Postdoc | CEA LIST, Université Paris-Saclay | |
| Jérôme Ricciardi | PhD student | CEA LIST, Université Paris-Saclay | Jérôme Ricciardi |
| Tomas Barros Carneiro | PhD student | CEA LIST, Université Paris-Saclay | Tomas Barros Carneiro |
Publications
International conference
- An Automated Deductive Verification Framework for Circuit-building Quantum Programs, March, 2021 at ESOP’21.
Book chapter
- Formal Methods for Quantum Algorithsms, 09/2023. This chapter introduces both the requirements and challenges for an efficient use of formal methods in quantum computing and the current most promising research directions. While the recent progress in quantum hardware opens the door for significant speedup in cryptography as well as additional key areas (biology, chemistry, optimization, machine learning, etc), quantum algorithms are still hard to implement right, and the validation of quantum programs is a challenge. As an alternative strategy, formal methods are prone to play a decisive role in the emerging field of quantum software. The chapter also introduces several existing solutions for the formal verification of quantum compilation and the equivalence of quantum program runs. The vast majority of quantum algorithms are described within the context of the quantum co-processor model, i.e. an hybrid model where a classical computer controls a quantum co-processor holding a quantum memory.
Preprint
- Toward certified quantum programming, March, 2020
Short articles
- 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)