We derive a variant of quantum Hoare logic (QHL), called applied quantum Hoare logic (aQHL for short), by: 1. restricting QHL to a special class of preconditions and postconditions, namely projections, which can significantly simplify verification of quantum programs and are much more convenient when used in debugging and testing; and 2. adding several rules for reasoning about robustness of quantum programs, i.e. error bounds of outputs. The effectiveness of aQHL is shown by its applications to verify two sophisticated quantum algorithms: HHL (Harrow-Hassidim-Lloyd) for solving systems of linear equations and qPCA (quantum Principal Component Analysis).
Wed 26 JunDisplayed time zone: Tijuana, Baja California change
Wed 26 Jun
Displayed time zone: Tijuana, Baja California change
10:00 - 11:00 | Verification IIPLDI Research Papers at 229AB Chair(s): Michael Norrish Data61 at CSIRO, Australia / Australian National University, Australia | ||
10:00 20mTalk | Verification of Programs under the Release-Acquire Semantics PLDI Research Papers Parosh Aziz Abdulla Uppsala University, Sweden, Jatin Arora IIT Bombay, India, Mohamed Faouzi Atig Uppsala University, Shankaranarayanan Krishna IIT Bombay, India | ||
10:20 20mTalk | A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture PLDI Research Papers Sandeep Dasgupta University of Illinois at Urbana-Champaign, USA, Daejun Park University of Illinois at Urbana-Champaign, Theodoros Kasampalis University of Illinois at Urbana-Champaign, USA, Vikram S. Adve University of Illinois at Urbana-Champaign, Grigore Roşu University of Illinois at Urbana-Champaign Link to publication DOI Pre-print Media Attached | ||
10:40 20mTalk | An Applied Quantum Hoare Logic PLDI Research Papers Li Zhou Department of Computer Science and Technology, Tsinghua University, Nengkun Yu University of Technology Sydney, Australia, Mingsheng Ying University of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University. Media Attached | ||