SpaceEx
From MaRDI portal
Software:22891
swMATH10939MaRDI QIDQ22891FDOQ22891
Author name not available (Why is that?)
Cited In (86)
- An Accurate Join for Zonotopes, Preserving Affine Input/Output Relations
- An Introduction to the Verification of Hybrid Systems Using Ariadne
- Data-driven and model-based verification via Bayesian identification and reachability analysis
- Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties
- Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction*
- A Practical Approach to Discretised PDDL+ Problems by Translation to Numeric Planning
- Safety preserving control synthesis for sampled data systems
- Fixpoint Computation in the Polyhedra Abstract Domain Using Convex and Numerical Analysis Tools
- A piecewise ellipsoidal reachable set estimation method for continuous bimodal piecewise affine systems
- Non-convex Invariants and Urgency Conditions on Linear Hybrid Automata
- Reachability analysis for high-index linear differential algebraic equations
- Abstraction based verification of stability of polyhedral switched systems
- Numerically-aided deductive safety proof for a powertrain control system
- Reachability of weakly nonlinear systems using Carleman linearization
- Formal System Verification
- Formal Verification Applied to Robotic Surgery
- Linear Hybrid System Falsification through Local Search
- Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro}
- An axiomatic approach to existence and liveness for differential equations
- Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point
- Decomposing reach set computations with low-dimensional sets and high-dimensional matrices (extended version)
- \textsf{IMITATOR} 3: synthesis of timing parameters beyond decidability
- Effective hybrid system falsification using Monte Carlo tree search guided by QB-robustness
- Verisig 2.0: verification of neural network controllers using Taylor model preconditioning
- Analysis on reachable set for spacecraft relative motion under low-thrust
- Event-B refinement for continuous behaviours approximation
- Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants
- Quantitative Model Checking for a Controller Design
- Finite state approximation for verification of partially observable stochastic hybrid systems
- Decomposition of Reachable Sets and Tubes for a Class of Nonlinear Systems
- Reachability Analysis of Nonlinear Differential-Algebraic Systems
- Eliminating spurious transitions in reachability with support functions
- Quasi-dependent variables in hybrid automata
- Reachability analysis of linear dynamic systems with constant, arbitrary, and Lipschitz continuous inputs
- Efficient geometric operations on convex polyhedra, with an application to reachability analysis of hybrid systems
- A survey of challenges for runtime verification from advanced application domains (beyond software)
- Efficient Bounded Reachability Computation for Rectangular Automata
- Lagrangian methods for approximating the viability kernel in high-dimensional systems
- A compositional modelling and analysis framework for stochastic hybrid systems
- Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration
- Template polyhedra and bilinear optimization
- \(\epsilon\)-semantics computations on biological systems
- A dynamic quantized state system execution framework for hybrid automata
- Pegasus: sound continuous invariant generation
- Rigorous Simulation-Based Analysis of Linear Hybrid Systems
- An improved algorithm for the control synthesis of nonlinear sampled switched systems
- Ariadne: Dominance Checking of Nonlinear Hybrid Automata Using Reachability Analysis
- Hybrid automata-based CEGAR for rectangular hybrid systems
- Verification of Hybrid Systems
- Computing branching distances with quantitative games
- Discretizing Affine Hybrid Automata with Uncertainty
- HYST
- JuliaReach
- Sapo
- TIRA
- Quantifier-free encoding of invariants for hybrid systems
- SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata
- Scalable Static Hybridization Methods for Analysis of Nonlinear Systems
- Reach Set Approximation through Decomposition with Low-dimensional Sets and High-dimensional Matrices
- Change-of-bases abstractions for non-linear hybrid systems
- Avoiding geometric intersection operations in reachability analysis of hybrid systems
- Satellite Rendezvous and Conjunction Avoidance: Case Studies in Verification of Nonlinear Hybrid Systems
- NLTOOLBOX: A Library for Reachability Computation of Nonlinear Dynamical Systems
- Forward Inner-Approximated Reachability of Non-Linear Continuous Systems
- Crossing the Bridge between Similar Games
- Counterexample-Guided Refinement of Template Polyhedra
- Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers
- Tracking smooth trajectories in linear hybrid systems
- Time-triggered conversion of guards for reachability analysis of hybrid automata
- Parameter synthesis of polynomial dynamical systems
- Extracting counterexamples induced by safety violation in linear hybrid systems
- Finite data-rate feedback stabilization of switched and hybrid linear systems
- Generalized property-directed reachability for hybrid systems
- Order-reduction abstractions for safety verification of high-dimensional linear systems
- Zélus
- Bellerophon: tactical theorem proving for hybrid systems
- Adaptive reachability algorithms for nonlinear systems using abstraction error analysis
- Formal verification and quantitative metrics of MPSoC data dynamics
- Construction of parametric barrier functions for dynamical systems using interval analysis
- Reachability analysis of a general class of neural ordinary differential equations
- Hybrid Automata-Based CEGAR for Rectangular Hybrid Systems
- Reachability Analysis of Polynomial Systems Using Linear Programming Relaxations
- Reachset Conformance Testing of Hybrid Automata
- Approximately bisimilar symbolic models for randomly switched stochastic systems
- ModelPlex: verified runtime validation of verified cyber-physical system models
- Reachability computation for polynomial dynamical systems
This page was built for software: SpaceEx