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.
Research-oriented internships, 4-6 months, 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: Logic and Verification, Quantum Programming [also: Programming Languages, Compilation]
Host: Commissariat à l’Énergie Atomique, Software Security Laboratory
Place: Paris-Saclay, France
Team: Qbricks
Advisor(s): Christophe Chareton, Nicolas Blanco, Sébastien Bardin (first.name@cea.fr)
Context. We are an emerging group in formal verification and static analysis of quantum programs, integrated in the Software Safety Laboratory of CEA List, Université Paris-Saclay.
Quantum hardware has made tremendous progress, and useful NISQ 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 for the standard 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. We are interested in these internships in verification mechanisms aiming at ensuring that a quantum program implementation indeed satisfies its intended behaviour. We propose the following topics:
- specification and verification of noisy quantum model
- high-level automatic verification of quantum programs for implicit program properties
- high-level functional reasoning for quantum programs
- circuit-level automatic verification of quantum programs, • …
More details on these topics will be happily provided! The list is not exhaustive, ask us if you have some project in mind.
All 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. Within CEA List, LSL is a forty-person team dedicated to software verification, with a strong focus on real-world applicability, industrial collaboration and industrial transfer. The quantum verification group is a young and emerging team. CEA List is located in Campus Paris Saclay.
Requirements: We welcome curious and enthusiastic students with a solid background in Computer Science, both theoretical and practical, and a specialization in either formal methods or quantum computing (note that we do not require candidates to have both expertises. it is assumed that the intern will dedicate some of her time upgrading her skills – included, if necessary, bases of quantum computing).
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
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 christophe.chareton@cea.fr as soon as possible (first come, first served). Candidates should send a CV, a cover letter, a transcript of all their university results, as well as contact information of two references.
Advisors: Christophe Chareton (CEA), Sébastien Bardin (CEA) Contact: christophe.chareton@cea.fr
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)