reachability

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
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
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
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
Computing Reachable Sets of Linear Vector Fields Revisited
The reachability problem is one of the most important issues in the verification of hybrid systems. But unfortunately the reachable …
PDF Cite Code Slides DOI
Computing Reachable Sets of Linear Vector Fields Revisited
Decidability of the Reachability for a Family of Linear Vector Fields
The reachability problem is one of the most important issues in the verification of hybrid systems. Computing the reachable sets of …
PDF Cite Code Slides DOI
Decidability of the Reachability for a Family of Linear Vector Fields