A SEMI-ALGEBRAIC APPROACH FOR THE COMPUTATION OF LYAPUNOV FUNCTIONS (2008)
In this paper we deal with the problem of computing Lyapunov functions for stability verification of differential systems. We concern on symbolic methods and start the discussion with a classical...
Recursive and Backward Reasoning in the Verification on Hybrid Systems ⋆ (2008)
Abstract. In this paper we introduce two improvements to the method of verification of hybrid systems by constraint propagation based abstraction refinement that we introduced earlier. The first...
Language-Based Abstraction Refinement for Hybrid System Verification ⋆ (2008)
Felix Klaedtke, Stefan Ratschan, Zhikun She
Abstract. The standard counterexample-guided abstraction-refinement (cegar) approach uses finite transition systems as abstractions of concrete systems. We present an approach to represent and refine...
Language-Based Abstraction Refinement for Hybrid System Verification ⋆ (2008)
Abstract. The standard counterexample-guided abstraction-refinement (cegar) approach uses finite transition systems as abstractions of concrete systems. We present an approach to represent and refine...
HSolver is a software package for the verification of safety properties of continuous time hybrid systems. It uses a method of constraint propagation based abstraction refinement [2, 1].
Safety Verification of Hybrid Systems by Constraint Propagation Based Abstraction Refinement (2007)
This paper deals with the problem of safety verification of nonlinear hybrid systems. We start from a classical method that uses interval arithmetic to check whether trajectories can move over the...
Providing a basin of attraction to a target region by computation of Lyapunov-like functions (2006)
In this paper, we present a method for computing a basin of attrac-tion to a target region for non-linear ordinary differential equations. This basin of attraction is ensured by a Lyapunov-like...
Providing a Basin of Attraction to a Target Region by Computation of Lyapunov-like Functions (2006)
In this paper, we present a method for computing a basin of attraction to a target region for non-linear ordinary differential equations. This basin of attraction is ensured by a Lyapunov-like...
A Semi-Algebraic Approach for the Computation of Lyapunov Functions (2006)
She, Zhikun, Xia, Bican, Xiao, Rong
In this paper we deal with the problem of computing Lya punov functions for stability verification of differential sys tems. We concern on symbolic methods and start the dis cussion with a classical...
Constraints for Continuous Reachability in the Verification of Hybrid Systems (2006)
Ratschan, Stefan, She, Zhikun, Calmet, Jacques, Ida, Tetsuo, Wang, Dongming
The method for verification of hybrid systems by constraint propagation based abstraction refinement that we introduced in an earlier paper is based on an over-approximation of continuous...
Safety verification of hybrid systems by constraint propagation based abstraction refinement (2005)
Abstract. This paper deals with the problem of safety verification of non-linear hybrid systems. We start from a classical method that uses interval arithmetic to check whether trajectories can move...
Safety Verification of Hybrid Systems by Constraint Propagation Based Abstraction Refinement (2005)
Ratschan, Stefan, She, Zhikun, Morari, Manfred, Thiele, Lothar
This paper deals with the problem of safety verification of non-linear hybrid systems. We start from a classical method that uses interval arithmetic to check whether trajectories can move over the...