We developed an extension of the analysis tool SpaceEx with integrated CEGAR (CounterExample Guided Abstraction Refinement) for the reachability analysis of hybrid systems.
Getting SpaceEx with CEGAR
The tool is released under the GPLv3.
We provide linux binaries which have been compiled on a 64bit Ubuntu.
The archive contains the binaries as well as a set of benchmarks.
Follow the README.txt to execute the benchmark files.
Click here to download the archive.
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.