verification

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 Poster 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
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
Taming Delays in Dynamical Systems
Delayed coupling between state variables occurs regularly in technical dynamical systems, especially embedded control. As it …
PDF Cite Slides DOI Artifact Evaluated
Taming Delays in Dynamical Systems