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
Friday, 11 July 2014
The team of Andreas Podelski at the University of Freiburg has made two extensions of SpaceEx available on their website.
Tuesday, 6 May 2014
A new prototype of the PHAVer scenario is now available.
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.