SpaceEx with CEGAR
We developed an extension of the analysis tool SpaceEx with integrated CEGAR (CounterExample Guided Abstraction Refinement) for the reachability analysis of hybrid systems.
Documentation
A technical report with a user manual can be downloaded here: technical report SpaceEx with CEGAR.
Third party libraries
We want to thank Goran Frehse and his development team for providing the analysis tool SpaceEx. Moreover, we want to thank the authors of the third-party libraries that are used by SpaceEx:
| Library | Version | Author(s) |
|---|---|---|
| Parma Polyhedra Library | 0.11.2 | Bagnara, P. M. Hill, E. Zaffanella |
| Boost.Program_options | 1.46.1 | |
| Boost.Regex | 1.46.1 | |
| GNU Multiple Precision Arithmetic Library | 5.0.2 | |
| GNU Linear Programming Kit | 4.45 | |
| SUNDIALS (Solver Suite) | 2.5.0 | Serban, C. Woodward, A. Hindmars |
| aaflib | 0.1 | |
| ublasJama | 1.0.2.2 | Frederic Devernay |
| TinyXML | 2.6.2 | Lee Thomason |
Authors
SpaceEx with CEGAR was developed and is maintained by Johanna Nellen, Erika Ábrahám and Benedikt Wolters.
Contact
For any questions, feedback and support requests regarding SpaceEx with CEGAR, please contact Johanna Nellen.