Document Open Access Logo

Qafny: A Quantum-Program Verifier (Artifact)

Authors Liyi Li , Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, Xiaodi Wu

PDF
Thumbnail PDF

Artifact Description

DARTS.10.2.12.pdf
  • Filesize: 432 kB
  • 2 pages

Document Identifiers

Author Details

Liyi Li
  • Iowa State University, Ames, IA, USA
Mingwei Zhu
  • University of Maryland, College Park, MD, USA
Rance Cleaveland
  • University of Maryland, College Park, MD, USA
Alexander Nicolellis
  • Iowa State University, Ames, IA, USA
Yi Lee
  • University of Maryland, College Park, MD, USA
Le Chang
  • University of Maryland, College Park, MD, USA
Xiaodi Wu
  • University of Maryland, College Park, MD, USA

Acknowledgements

We thank Finn Voichick for his helpful comments and contributions during the work’s development. This paper is dedicated to the memory of our dear co-author Rance Cleaveland.

Cite As Get BibTex

Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu. Qafny: A Quantum-Program Verifier (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 12:1-12:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/DARTS.10.2.12

Artifact

  MD5 Sum: e0d87be118b5024f66029dfe85695be5 (Get MD5 Sum)

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2024 Call for Artifacts and the ACM Artifact Review and Badging Policy.

Abstract

This artifact contains the Coq theory files for the Qafny proof system, including the formalism of the Qafny syntax, semantics, type system, and proof system, with the theorem proofs of type soundness, proof system soundness and completeness. It also contains a the compiled Dafny example programs generated from our Qafny-to-Dafny prototype compiler. These example programs serve as the validations of our Qafny-to-Dafny prototype compiler mechanism. The main work is introduced in the Qafny paper, which develops a separation logic style verification framework for quantum programs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program verification
  • Theory of computation → Quantum information theory
Keywords
  • Quantum Computing
  • Automated Verification
  • Separation Logic

Metrics

Related Article

  • Liyi Li, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Le Chang, and Xiaodi Wu, "Qafny: A Quantum-Program Verifier", in 38th European Conference on Object-Oriented Programming (ECOOP 2024), LIPIcs, Vol. 313, pp. 24:1-24:31, 2024. https://doi.org/10.4230/LIPIcs.ECOOP.2024.24
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact