uncertainty

Tolerant Barrier Certificates for Stochastic Systems
We study stochastic verification under tolerant specifications, where unsafe behavior is allowed as long as the total unsafe exposure …
Cite
Tolerant Barrier Certificates for Stochastic Systems
Fixed-Point Reasoning for Stochastic Systems
Fixed points are mathematical objects that are commonly employed in computer science to characterize key properties of iterative or …
PDF Cite
Fixed-Point Reasoning for Stochastic Systems
On Termination of Polynomial Programs with Equality Conditions
We investigate the termination problem of a family of multi-path polynomial programs (MPPs) over a general field $\mathbb{K}$, in which …
Cite Code DOI
On Termination of Polynomial Programs with Equality Conditions
On the Almost-Sure Termination of Probabilistic Counter Programs
This paper introduces $k$-d PCPs – the class of probabilistic counter programs with $k \in \mathbb{N}$ counter variables inducing …
PDF Cite DOI Artifact Evaluated
On the Almost-Sure Termination of Probabilistic Counter Programs
Vegapunk: Accurate and Fast Decoding for Quantum LDPC Codes with Online Hierarchical Algorithm and Sparse Accelerator
Quantum Low-Density Parity-Check (qLDPC) codes are a promising class of quantum error-correcting codes that exhibit constant-rate …
Cite
Vegapunk: Accurate and Fast Decoding for Quantum LDPC Codes with Online Hierarchical Algorithm and Sparse Accelerator
YOUTIAO: Hybrid Multiplexing with Dynamic Qubit Grouping for Low-cost and Scalable Quantum Wiring
With continuous advances in physical technology, the number of qubits has increased from just a few to several thousand. To further …
Cite
YOUTIAO: Hybrid Multiplexing with Dynamic Qubit Grouping for Low-cost and Scalable Quantum Wiring
AdaptDQC: Adaptive Distributed Quantum Computing with Quantitative Performance Analysis
We present AdaptDQC, an adaptive compiler framework for optimizing distributed quantum computing (DQC) under diverse performance …
Cite
AdaptDQC: Adaptive Distributed Quantum Computing with Quantitative Performance Analysis
Fast-USYN: Fast Synthesis from Unitary Matrices to High-Quality Quantum Circuits
Current quantum programs are usually represented as quantum circuits, including various quantum gates. If the program contains gates …
PDF Cite
Fast-USYN: Fast Synthesis from Unitary Matrices to High-Quality Quantum Circuits
A Unified Framework for Quantitative Analysis of Probabilistic Programs
Verifying probabilistic programs requires reasoning about various probabilistic behaviors, e.g., random sampling, nondeterminism, and …
PDF Cite DOI
A Unified Framework for Quantitative Analysis of Probabilistic Programs
MorphQPV: Exploiting Isomorphism in Quantum Programs to Facilitate Confident Verification
Unlike classical computing, quantum program verification (QPV) is much more challenging due to the non-duplicability of quantum states …
PDF Cite Code DOI Artifact Evaluated
MorphQPV: Exploiting Isomorphism in Quantum Programs to Facilitate Confident Verification