@inproceedings{FLD+1,
title = { SpaceEx: Scalable Verification of Hybrid Systems },
author = {Frehse, Goran and Le Guernic, Colas and Donz\'e, Alexandre and Cotton, Scott and Ray, Rajarshi and Lebeltel, Olivier and Ripado, Rodolfo and Girard, Antoine and Dang, Thao and Maler, Oded},
year = {2011},
booktitle = {Proc. 23rd International Conference on Computer Aided Verification (CAV)},
publisher = {Springer},
series = {LNCS},
team = {axe_Mohytos, TEMPO},
abstract = {We present a scalable reachability algorithm for hybrid systems with piecewise affine, non-deterministic dynamics. It combines polyhedra and support function representations of continuous sets to compute an overapproximation of the reachable states. The algorithm improves over previous work by using variable time steps to guarantee a given local error bound. In addition, we propose an improved approximation model, which drastically improves the accuracy of the algorithm. The algorithm is implemented as part of SpaceEx, a new veri cation platform for hybrid systems, available at spaceex.imag.fr. Experimental results of full fixed-point computations with hybrid systems with more than 100 variables illustrate the scalability of the approach.},
}
