SpaceEx State Space Explorer

The verification of continuous and hybrid systems is a challenging problem, and various approaches are currently being investigated to overcome the complexities of representing and computing with continuous sets of states. Since verification problems are generally undecidable for such systems, experimental results are vital for evaluating and developing new ideas.

The SpaceEx tool platform is designed to facilitate the implementation of algorithms related to reachability and safety verification.

Examples and Tutorials

Frequently Asked Questions

This document provides some answers to common questions about SpaceEx.

Introduction to SpaceEx

This document provides a brief overview of the capabilities of SpaceEx and the concepts behind...

Latest News
Friday, 3 August 2018
The SL2SX translator is now available at:
Wednesday, 9 March 2016
A semi-automatic translation tool from Simlink to SpaceEx, called SL2SX, is now available as a beta-version from
Thursday, 9 July 2015
A bugfix update for SpaceEx is now available for download. A major bug has been fixed that could lead to wrong reachability results, so an update is strongly recommended.