Introduction to SpaceEx

This document provides a brief overview of the capabilities of SpaceEx and the concepts behind it.
We present how hybrid systems are modeled in SpaceEx using hybrid automata that can be composed in nested networks.
We give an overview of the analysis algorithms implemented in SpaceEx, and the different options that are available to the user.
The algorithms are described strictly from a user perspective, mentioning mathematical details and algorithmic trickery only when necessary.
The reader is assumed to be familiar with the basic concepts of hybrid systems and reachability analysis.
For brevity, the presentation is informal, but references to more detailed descriptions are given in the text.