Equation Relaxation-based Barrier-like Condition Construction Methods
Preprint
-
Refined Barrier Conditions for Finite-Time Safety and Reach-Avoid Guarantees in Stochastic Systems2025 Arxiv
-
Controlled Reach-avoid Set Computation for Discrete-time Polynomial Systems via Convex Optimization2025 Arxiv
-
Sufficient and Necessary Barrier-like Conditions for Safety and Reach-avoid Verification of Stochastic Discrete-time Systems2024 Arxiv
-
A Framework for Safe Probabilistic Invariance Verification of Stochastic Dynamical Systems2024 Arxiv
-
Converse Barrier Certificates for Finite-time Safety Verification of Continuous-time Perturbed Deterministic Systems2024 Arxiv
-
Reachability Verification for Stochastic Discrete-time Dynamical Systems2023 Arxiv
Journal Papers
-
A New Framework for Bounding Reachability Probabilities of Continuous-time Stochastic Systems2025Nonlinear Analysis: Hybrid Systems
-
Finite-time Safety and Reach-avoid Verification of Stochastic Discrete-time Systems2025 Information and Computation
-
Reach-avoid Controllers Synthesis for Safety Critical Systems2024 IEEE Transactions on Automatic Control
-
Reach-Avoid Analysis for Polynomial Stochastic Differential Equations2024 IEEE Transactions on Automatic Control
-
Reach-avoid Verification Based on Convex Optimization2024 IEEE Transactions on Automatic Control
-
Inner-approximating Robust Reach-avoid Sets for Discrete-time Polynomial Dynamical Systems2023 IEEE Transactions on Automatic Control
-
Synthesizing Robust Domains of Attraction for State-Constrained Perturbed Polynomial Systems2021 SIAM Journal on Control and Optimization
-
Safety Verification for Random Ordinary Differential Equations2020 IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
-
Inner-Approximating Reachable Sets for Polynomial Systems with Time-Varying Uncertainties2020 IEEE Transactions on Automatic Control
-
Robust Invariant Sets Computation for Discrete-Time Perturbed Nonlinear Systems2022 IEEE Transactions on Automatic Control
Conference Papers
-
Provable Reach-avoid Controllers Synthesis Based on Inner-approximating Controlled Reach-avoid Sets2025 Festschrift of Prof. Martin Fränzle's 60th birthday
-
Safe Exit Controllers Synthesis for Continuous-time Stochastic Systems2024 CDC
-
An Iterative Method for Computing Controlled Reach-avoid sets2024 ACC
-
Reach-avoid Analysis for Sampled-data Systems with Measurement Uncertainties2024 ACC
-
Reach-avoid Verification Using Lyapunov Densities2024 Chinese Control Conference
-
Safe Probabilistic Invariance Verification for Stochastic Discrete-time Dynamical Systems2023 CDC
-
Model Predictive Control with Reach-Avoid Analysis2023 IJCAI
-
Outer-approximating Controlled Reach-avoid Sets for Polynomial Systems2022 CDC
-
Differential Games Based on Invariant Sets Generation2022 ACC
-
Reach-avoid Analysis for Delay Differential Equations2021 CDC
-
Reach-avoid Analysis for Stochastic Discrete-time Systems2021 ACC
-
Inner-approximating Reach-avoid Sets for Discrete-time Polynomial Systems2020 CDC
-
Robust Regions of Attraction Generation for State-Constrained Perturbed Discrete-Time Polynomial Systems2020 IFAC
-
A Characterization of Robust Regions of Attraction for Discrete-Time Systems Based on Bellman Equations2020 IFAC
-
Robust invariant sets generation for state-constrained perturbed polynomial systems2019 HSCC
-
Under-Approximating Reach Sets for Polynomial Continuous Systems2018 HSCC
-
Robust Non-termination Analysis of Numerical Software2018 SETTA (Best paper awards)
Set-boundary Propagation Reachability Methods (Tool: PyBDR and BdryReach)
Journal Papers
-
Verifying Safety of Neural Networks from Topological Perspectives2024 Science of Computer Programming
-
Over- and Underapproximating Reach Sets for Perturbed Delay Differential Equations2021 IEEE Transactions on Automatic Control
-
Reach-Avoid Verification for Nonlinear Systems Based on Boundary Analysis2017 IEEE Transactions on Automatic Control
-
Underapproximating Backward Reachable Sets by Semialgebraic Sets2017 IEEE Transactions on Automatic Control
Conference Papers
-
PyBDR: Set-boundary based Reachability Analysis Toolkit in Python2024 International Symposium on Formal Methods
-
Inner-approximate Reachability Computation via Zonotopic Boundary Analysis2024 International Conference on Computer Aided Verification
-
Safety Verification for Neural Networks Based on Set-boundary Analysis2023 International Symposium on Theoretical Aspects of Software Engineering
-
Safe Over- and Under-Approximation of Reachable Sets for Delay Differential Equations2017 FORMATS
-
Under-Approximating Backward Reachable Sets by Polytopes2016 CAV
-
Just scratching the surface: Partial exploration of initial values in reach-set computation2017 CDC
PAC Learning-driven Reachability Methods
Preprint
-
Convex Computations for Controlled Safety Invariant Sets of Black-box Discrete-time Dynamical Systems2025 Arxiv
Journal Papers
-
PAC Model Checking of Black-Box Continuous-Time Dynamical Systems2020 IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems
Conference Papers
-
Towards Practical Robustness Analysis for DNNs based on PAC-Model Learning2022 International Conference on Software Engineering
-
Safe Inputs Approximation for Black-Box Systems2019 ICECCS
-
Probably Approximate Safety Verification of Hybrid Dynamical Systems2019 ICFEM
Other Publications
Journal Papers
-
Automatic Verification of Bounded Synchronization for Heterogeneous Polynomial Networked Systems2024 IEEE Transactions on Automatic Control
-
Consensus Criterion Verification for Heterogeneous Multi-Agent Systems via Sum-of-Squares Programming2024 IEEE Transactions on Automatic Control
-
Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming2022 Information and Computation
-
Qualitative and Quantitative Model Checking against Recurrent Neural Networks2023 Journal of Computer Science and Technology
-
Stability Verification for Heterogeneous Complex Networks via Iterative SOS Programming2022 IEEE Control Systems Letters
-
Consensus Control for Heterogeneous Multi-vehicle Systems: An Iterative Learning Approach2021 IEEE Transactions on Neural Networks and Learning Systems
-
Discovering polynomial Lyapunov functions for continuous dynamical systems2013 Journal of Symbolic Computation
-
Discovering Multiple Lyapunov Functions for Switched Hybrid Systems2014 SIAM Journal on Control and Optimization
Conference Papers
-
Efficient Verification and Falsification of ReLU Neural Barrier Certificates2025 AAAI
-
Improving Neural Network Verification through Spurious Region Guided Refinement2021 TACAS
-
PRODEEP: a platform for robustness verification of deep neural networks2020 ESEC/FSE
-
Synthesizing Invariant Barrier Certificates via Difference-of-Convex Programming2021 CAV
-
Unbounded-Time Safety Verification of Stochastic Differential Dynamics2020 CAV
-
Taming delays in dynamical systems: Unbounded verification of delay differential equations2019 CAV
-
Brief Industry Paper: Modeling and Verification of Descent Guidance Control of Mars Lander2021 RTAS
-
Switching Controller Synthesis for Delay Hybrid Systems under Perturbations2021 HSCC
-
Nonlinear Craig Interpolant Generation2020 CAV
-
Probably Approximately Correct Interpolants Generation2020 SETTA
-
Safe Over- and Under-Approximation of Reachable Sets for Autonomous Dynamical Systems2018 FORMATS
-
PAC Learning of Deterministic One-Clock Timed Automata2020 ICFEM
-
Linearization based Safety Verification of a Glucose Control Protocol2019 ISORC
-
Model Checking Delay Differential Equations Against Metric Interval Temporal Logic2017 Scientific Annals of Computer Science
-
Algebraic Analysis on Asymptotic Stability of Continuous Dynamical Systems2011 ISSAC
-
Algebraic Analysis on Asymptotic Stability of Switched Hybrid Systems2012 HSCC
-
Discovering multiple Lyapunov functions for switched hybrid systems with global exponential stability2015 CDC