1

QuFEM: Fast and Accurate Quantum Readout Calibration Using the Finite Element Method
Quantum readout error turns out to be the most significant error source, which greatly affects the measurement fidelity. Matrix-based …
Cite
QuFEM: Fast and Accurate Quantum Readout Calibration Using the Finite Element Method
PS3: Precise Patch Presence Test Based on Semantic Symbolic Signature
During software development, vulnerabilities have posed a significant threat to users. Applying patches is the most effective way to …
Cite
PS3: Precise Patch Presence Test Based on Semantic Symbolic Signature
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Essential tasks for the verification of probabilistic programs include bounding expected outcomes and proving termination in finite …
PDF Cite DOI Artifact Evaluated
Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants
Exact Probabilistic Inference Using Generating Functions
Probabilistic programs are typically normal-looking programs describing posterior probability distributions. They intrinsically code up …
PDF Cite Code
Exact Probabilistic Inference Using Generating Functions
Does a Program Yield the Right Distribution?
We study discrete probabilistic programs with potentially unbounded looping behaviors over an infinite state space. We present, to the …
PDF Cite DOI Artifact Evaluated
Does a Program Yield the Right Distribution?
Latticed $k$-Induction with an Application to Probabilistic Programs
We revisit two well-established verification techniques, $k$-induction and bounded model checking (BMC), in the more general setting of …
PDF Cite Slides DOI Artifact Evaluated Pulp Fiction
Latticed $k$-Induction with an Application to Probabilistic Programs
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
A barrier certificate often serves as an inductive invariant that isolates an unsafe region from the reachable set of states, and hence …
PDF Cite Slides Video DOI Artifact Evaluated
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming
Unbounded-Time Safety Verification of Stochastic Differential Dynamics
In this paper, we propose a method for bounding the probability that a stochastic differential equation (SDE) system violates a safety …
PDF Cite Slides Video DOI Artifact Evaluated Pulp Fiction
Unbounded-Time Safety Verification of Stochastic Differential Dynamics
Learning One-Clock Timed Automata
We present an algorithm for active learning of deterministic timed automata with a single clock. The algorithm is within the framework …
PDF Cite Slides DOI Artifact Evaluated Best Paper Award @ FMAC 2019 Springer High-Impact Paper
Learning One-Clock Timed Automata
NIL: Learning Nonlinear Interpolants
Nonlinear interpolants have been shown useful for the verification of programs and hybrid systems in contexts of theorem proving, model …
PDF Cite Code Slides DOI
NIL: Learning Nonlinear Interpolants