Formal verification

A Verified Optimizer for Quantum Circuits
We present voqc, the first verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are …
Kesha Hietala, Robert Rand, Liyi Li, Shih-Han Hung, Xiaodi Wu, Michael Hicks
Cite DOI URL
Models for Probabilistic Programs with an Adversary
Robert Rand, Steve Zdancewic
PDF Slides
Verifying Probabilistic Programs in the Presence of an Adversary
3rd place in the graduate student poster competition.
Robert Rand
Slides Video Poster
VPHL: A Verified Partial-Correctness Logic for Probabilistic Programs
We introduce a Hoare-style logic for probabilistic programs, called VPHL, that has been formally verified in the Coq proof assistant. …
Robert Rand, Steve Zdancewic
PDF Cite Slides DOI