safety

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
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
Indecision and Delays are the Parents of Failure
The possible interactions between a controller and its environment can naturally be modelled as the arena of a two-player game, and …
PDF Cite Code Slides Video DOI
Indecision and Delays are the Parents of Failure
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
What's to Come is Still Unsure
The possible interactions between a controller and its environment can naturally be modelled as the arena of a two-player game, and …
PDF Cite Code Slides Video DOI Distinguished Paper Award
What's to Come is Still Unsure
Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations
Delays in feedback control loop, as induced by networked distributed control schemes, may have detrimental effects on control …
PDF Cite Slides Video DOI
Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations
Validated Simulation-Based Verification of Delayed Differential Dynamics
Verification by simulation, based on covering the set of time-bounded trajectories of a dynamical system evolving from the initial …
PDF Cite Code Poster Slides DOI
Validated Simulation-Based Verification of Delayed Differential Dynamics