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.

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.


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 Frederic Devernay
TinyXML 2.6.2 Lee Thomason


SpaceEx with CEGAR was developed and is maintained by Johanna NellenErika Ábrahám and Benedikt Wolters.


For any questions, feedback and support requests regarding SpaceEx with CEGAR, please contact Johanna Nellen.