verification

Exact Bayesian Inference for Loopy Probabilistic Programs
We present an exact Bayesian inference method for inferring posterior distributions encoded by probabilistic programs featuring …
PDF Cite Code DOI
Exact Bayesian Inference for Loopy Probabilistic Programs
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
Lower Bounds for Possibly Divergent Probabilistic Programs
We present a new proof rule for verifying lower bounds on quantities of probabilistic programs. Our proof rule is not confined to …
PDF Cite Slides DOI
Lower Bounds for Possibly Divergent Probabilistic Programs
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
Encoding Inductive Invariants as Barrier Certificates
We present the invariant barrier-certificate condition that witnesses unbounded-time safety of differential dynamical systems. The …
PDF Cite Code Slides DOI
Encoding Inductive Invariants as Barrier Certificates
PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot
Hardware supply-chain attacks are raising significant security threats to the boot process of multiprocessor systems. This paper …
PDF Cite DOI
PA-Boot: A Formally Verified Authentication Protocol for Multiprocessor Secure Boot
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