10 citations · 15 across the 6 of their papers we have counts for
7 papers
Synthesis of Compact and Expressive Quantum-Circuit Optimizations
Wei Qiang, Ronghui Gu
Today's quantum devices are noisy, so reducing circuit size is critical for reliable execution. Existing rule-based optimizers often rely on large rule sets that are difficult to m…
Giallar: Push-Button Verification for the Qiskit Quantum Compiler
Runzhou Tao, Yunong Shi, Jianan Yao +5
This paper presents Giallar, a fully-automated verification toolkit for quantum compilers. Giallar requires no manual specifications, invariants, or proofs, and can automatically v…
Gleipnir: Toward Practical Error Analysis for Quantum Programs (Extended Version)
Runzhou Tao, Yunong Shi, Jianan Yao +3
Practical error analysis is essential for the design, optimization, and evaluation of Noisy Intermediate-Scale Quantum(NISQ) computing. However, bounding errors in quantum programs…
SciviK: A Versatile Framework for Specifying and Verifying Smart Contracts
Shaokai Lin, Xinyuan Sun, Jianan Yao +1
The growing adoption of smart contracts on blockchains poses new security risks that can lead to significant monetary loss, while existing approaches either provide no (or partial)…
Learning Nonlinear Loop Invariants with Gated Continuous Logic Networks (Extended Version)
Jianan Yao, Gabriel Ryan, Justin Wong +2
Verifying real-world programs often requires inferring loop invariants with nonlinear constraints. This is especially true in programs that perform many numerical operations, such…
CLN2INV: Learning Loop Invariants with Continuous Logic Networks
Gabriel Ryan, Justin Wong, Jianan Yao +2
Program verification offers a framework for ensuring program correctness and therefore systematically eliminating different classes of bugs. Inferring loop invariants is one of the…