Home
News
People
Publications
Courses
Vacancies
Contact
Pulp Fictions
Light
Dark
Automatic
barrier certificates
Encoding Inductive Invariants as Barrier Certificates
We present the
invariant barrier-certificate condition
that witnesses unbounded-time safety of differential dynamical systems. The …
Qiuye Wang
,
Mingshuai Chen
,
Bai Xue
,
Naijun Zhan
,
Joost-Pieter Katoen
PDF
Cite
Code
Slides
DOI
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 …
Qiuye Wang
,
Mingshuai Chen
,
Bai Xue
,
Naijun Zhan
,
Joost-Pieter Katoen
PDF
Cite
Slides
Video
DOI
Artifact Evaluated
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 …
Shenghua Feng
,
Mingshuai Chen
,
Bai Xue
,
Sriram Sankaranarayanan
,
Naijun Zhan
PDF
Cite
Slides
Video
DOI
Artifact Evaluated
Pulp Fiction
Cite
×