Assume-guarantee verification of nonlinear hybrid systems with ARIADNE
From MaRDI portal
Publication:5408048
Recommendations
- An introduction to the verification of hybrid systems using \textsc{Ariadne}
- Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis
- Safety verification of non-linear hybrid systems is quasi-semidecidable
- Safety verification of non-linear hybrid systems is quasi-decidable
- GUARANTEED TERMINATION IN THE VERIFICATION OF LTL PROPERTIES OF NON-LINEAR ROBUST DISCRETE TIME HYBRID SYSTEMS
Cites work
- scientific article; zbMATH DE number 1460545 (Why is no real title available?)
- Abstraction and Counterexample-Guided Refinement in Model Checking of Hybrid Systems
- Abstractions for hybrid systems
- An Approach to Modelling and Verification of Component Based Systems
- An introduction to Kolmogorov complexity and its applications
- Continuity and computability of reachable sets
- Graph-Based Algorithms for Boolean Function Manipulation
- HyTech: A model checker for hybrid systems
- Hybrid I/O automata.
- KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
- Kronos: A verification tool for real-time systems
- Semantics and computability of the evolution of hybrid systems
- Solutions to hybrid inclusions via set and graphical convergence with stability theory applications
- The algorithmic analysis of hybrid systems
- Uppaal in a nutshell
- What's decidable about hybrid automata?
Cited in
(13)- Formal Verification Applied to Robotic Surgery
- Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system
- The ksmt calculus is a \(\delta \)-complete decision procedure for non-linear constraints
- Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
- A dynamic quantized state system execution framework for hybrid automata
- A computable and compositional semantics for hybrid systems
- Proving the existence of fair paths in infinite-state systems
- An introduction to the verification of hybrid systems using \textsc{Ariadne}
- The \texttt{ksmt} calculus is a \(\delta \)-complete decision procedure for non-linear constraints
- Constraint-driven nonlinear reachability analysis with automated tuning of tool properties
- Ariadne: dominance checking of nonlinear hybrid automata using reachability analysis
- Adaptive reachability algorithms for nonlinear systems using abstraction error analysis
- Adaptive parameter tuning for reachability analysis of nonlinear systems
This page was built for publication: Assume-guarantee verification of nonlinear hybrid systems with ARIADNE
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5408048)
