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...

Installing the SpaceEx VM Server

The SpaceEx Virtual Machine (VM) allows you to run the SpaceEx platform...

Latest News
Thursday, 7 November 2013
This update improves the numerical stability of LGG and STC reachability algorithms and fixes a major bug from the previous release.
Tuesday, 15 October 2013
The latest update of SpaceEx introduces major improvements and new features.
Monday, 26 November 2012
A new analysis algorithm is available on the SpaceEx platform: The STC scenario produces fewer convex sets for a given accuracy and computes more precise images of discrete transitions.