Wed 26 Jun 2019 10:40 - 11:00 at 229AB - Verification II Chair(s): Michael Norrish

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 Jun
Times are displayed in time zone: Tijuana, Baja California change

10:00 - 11:00: Verification IIPLDI Research Papers at 229AB
Chair(s): Michael NorrishData61 at CSIRO, Australia / Australian National University, Australia
10:00 - 10:20
Talk
Verification of Programs under the Release-Acquire Semantics
PLDI Research Papers
Parosh Aziz AbdullaUppsala University, Sweden, Jatin AroraIIT Bombay, India, Mohamed Faouzi AtigUppsala University, Shankaranarayanan KrishnaIIT Bombay, India
10:20 - 10:40
Talk
A Complete Formal Semantics of x86-64 User-Level Instruction Set Architecture
PLDI Research Papers
Sandeep DasguptaUniversity of Illinois at Urbana-Champaign, USA, Daejun ParkUniversity of Illinois at Urbana-Champaign, Theodoros KasampalisUniversity of Illinois at Urbana-Champaign, USA, Vikram S. AdveUniversity of Illinois at Urbana-Champaign, Grigore Ro┼čuUniversity of Illinois at Urbana-Champaign
Link to publication DOI Pre-print Media Attached
10:40 - 11:00
Talk
An Applied Quantum Hoare Logic
PLDI Research Papers
Li ZhouDepartment of Computer Science and Technology, Tsinghua University, Nengkun YuUniversity of Technology Sydney, Australia, Mingsheng YingUniversity of Technology Sydney, Australia / Institute of Software at Chinese Academy of Sciences, China/ Department of Computer Science and Technology, Tsinghua University.
Media Attached