verification

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
Verification and Synthesis of Time-Delayed Dynamical Systems
Conventional embedded systems have over the past two decades vividly evolved into an open, interconnected form that integrates …
Cite Slides CAS-President Special Award
Verification and Synthesis of Time-Delayed Dynamical Systems
In Memory of Oded Maler: Automatic Reachability Analysis of Hybrid-State Automata
Hybrid automata are an elegant formal model seamlessly integrating differential equations representing continuous dynamics with …
PDF Cite DOI
In Memory of Oded Maler: Automatic Reachability Analysis of Hybrid-State Automata
Reachability Analysis for Solvable Dynamical Systems
The reachability problem is one of the most important issues in the verification of hybrid systems. But unfortunately the reachable …
PDF Cite Code DOI
Reachability Analysis for Solvable Dynamical Systems