An Automated Deductive Verification Framework for Circuit-Building Quantum Programs. Chareton, C., Bardin, S., Bobot, F., Perrelle, V., & Valiron, B. In Programming Languages and Systems, ESOP 2021, volume 12648, of Lecture Notes in Computer Science, pages 148–177, Cham, March, 2021. Springer International Publishing. doi abstract bibtex While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose Qbricks, a formal verification environment for circuit-building quantum programs, featuring both parametric specifications and a high degree of proof automation. We propose a logical framework based on first-order logic, and develop the main tool we rely upon for achieving the automation of proofs of quantum specification: PPS, a parametric extension of the recently developed path sum semantics. To back-up our claims, we implement and verify parametric versions of several famous and non-trivial quantum algorithms, including the quantum parts of Shor's integer factoring, quantum phase estimation (QPE) and Grover's search.
@inproceedings{Chareton2021,
title = {An Automated Deductive Verification Framework for Circuit-Building Quantum Programs},
author = {Chareton, Christophe and Bardin, S{\'e}bastien and Bobot, Fran{\c c}ois and Perrelle, Valentin and Valiron, Beno{\^i}t},
year = {2021},
month = mar,
booktitle = {Programming Languages and Systems, ESOP 2021},
editor = {Yoshida, Nobuko},
publisher = sprintl,
address = {{Cham}},
series = {Lecture Notes in Computer Science},
volume = {12648},
pages = {148--177},
doi = {10.1007/978-3-030-72019-3_6},
archiveprefix = {arXiv},
eprint = {2003.05841},
abstract = {While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose Qbricks, a formal verification environment for circuit-building quantum programs, featuring both parametric specifications and a high degree of proof automation. We propose a logical framework based on first-order logic, and develop the main tool we rely upon for achieving the automation of proofs of quantum specification: PPS, a parametric extension of the recently developed path sum semantics. To back-up our claims, we implement and verify parametric versions of several famous and non-trivial quantum algorithms, including the quantum parts of Shor's integer factoring, quantum phase estimation (QPE) and Grover's search.},
keywords = {deductive verification, quantum programming, quantum circuits, sum-over-paths},
webnote = {See extended version on arXiv for additional technical material.},
bibsource = qplbib
}
Downloads: 0
{"_id":"fCRJDev3ATNgcFSXj","bibbaseid":"chareton-bardin-bobot-perrelle-valiron-anautomateddeductiveverificationframeworkforcircuitbuildingquantumprograms-2021","author_short":["Chareton, C.","Bardin, S.","Bobot, F.","Perrelle, V.","Valiron, B."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"An Automated Deductive Verification Framework for Circuit-Building Quantum Programs","author":[{"propositions":[],"lastnames":["Chareton"],"firstnames":["Christophe"],"suffixes":[]},{"propositions":[],"lastnames":["Bardin"],"firstnames":["Sébastien"],"suffixes":[]},{"propositions":[],"lastnames":["Bobot"],"firstnames":["Fran ̧cois"],"suffixes":[]},{"propositions":[],"lastnames":["Perrelle"],"firstnames":["Valentin"],"suffixes":[]},{"propositions":[],"lastnames":["Valiron"],"firstnames":["Benoît"],"suffixes":[]}],"year":"2021","month":"March","booktitle":"Programming Languages and Systems, ESOP 2021","editor":[{"propositions":[],"lastnames":["Yoshida"],"firstnames":["Nobuko"],"suffixes":[]}],"publisher":"Springer International Publishing","address":"Cham","series":"Lecture Notes in Computer Science","volume":"12648","pages":"148–177","doi":"10.1007/978-3-030-72019-3_6","archiveprefix":"arXiv","eprint":"2003.05841","abstract":"While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose Qbricks, a formal verification environment for circuit-building quantum programs, featuring both parametric specifications and a high degree of proof automation. We propose a logical framework based on first-order logic, and develop the main tool we rely upon for achieving the automation of proofs of quantum specification: PPS, a parametric extension of the recently developed path sum semantics. To back-up our claims, we implement and verify parametric versions of several famous and non-trivial quantum algorithms, including the quantum parts of Shor's integer factoring, quantum phase estimation (QPE) and Grover's search.","keywords":"deductive verification, quantum programming, quantum circuits, sum-over-paths","webnote":"See extended version on arXiv for additional technical material.","bibsource":"Quantum Programming Languages & Verification Bibliography, https://git.io/qpl-bib","bibtex":"@inproceedings{Chareton2021,\n title = {An Automated Deductive Verification Framework for Circuit-Building Quantum Programs},\n author = {Chareton, Christophe and Bardin, S{\\'e}bastien and Bobot, Fran{\\c c}ois and Perrelle, Valentin and Valiron, Beno{\\^i}t},\n year = {2021},\n month = mar,\n booktitle = {Programming Languages and Systems, ESOP 2021},\n editor = {Yoshida, Nobuko},\n publisher = sprintl,\n address = {{Cham}},\n series = {Lecture Notes in Computer Science},\n volume = {12648},\n pages = {148--177},\n doi = {10.1007/978-3-030-72019-3_6},\n archiveprefix = {arXiv},\n eprint = {2003.05841},\n abstract = {While recent progress in quantum hardware open the door for significant speedup in certain key areas, quantum algorithms are still hard to implement right, and the validation of such quantum programs is a challenge. In this paper we propose Qbricks, a formal verification environment for circuit-building quantum programs, featuring both parametric specifications and a high degree of proof automation. We propose a logical framework based on first-order logic, and develop the main tool we rely upon for achieving the automation of proofs of quantum specification: PPS, a parametric extension of the recently developed path sum semantics. To back-up our claims, we implement and verify parametric versions of several famous and non-trivial quantum algorithms, including the quantum parts of Shor's integer factoring, quantum phase estimation (QPE) and Grover's search.},\n keywords = {deductive verification, quantum programming, quantum circuits, sum-over-paths},\n webnote = {See extended version on arXiv for additional technical material.},\n bibsource = qplbib\n}\n\n","author_short":["Chareton, C.","Bardin, S.","Bobot, F.","Perrelle, V.","Valiron, B."],"editor_short":["Yoshida, N."],"key":"Chareton2021","id":"Chareton2021","bibbaseid":"chareton-bardin-bobot-perrelle-valiron-anautomateddeductiveverificationframeworkforcircuitbuildingquantumprograms-2021","role":"author","urls":{},"keyword":["deductive verification","quantum programming","quantum circuits","sum-over-paths"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://raw.githubusercontent.com/QuantumPL/bib/main/bbt.bib","dataSources":["JG9W34HAXfSxsC6ML"],"keywords":["deductive verification","quantum programming","quantum circuits","sum-over-paths"],"search_terms":["automated","deductive","verification","framework","circuit","building","quantum","programs","chareton","bardin","bobot","perrelle","valiron"],"title":"An Automated Deductive Verification Framework for Circuit-Building Quantum Programs","year":2021}