SpaceEx State Space Explorer

Third Party Developments and Links

University of Freiburg

SpaceEx with Guided Search

Guiding the search with a pattern database

SpaceEx with guided search integrates a number of new search schemas adjusted towards finding an error path in the state space. The first option is a simple DFS search which terminates as soon as the intersection with the bad state has been detected. The other new option we provide is the box-based heuristic. This is a light-weight heuristic which prioritizes the successor symbolic states based on their continuous part. Finally, we introduce an abstraction-based cost function based on pattern databases for guiding the reachability analysis. For this purpose, we introduce a suitable abstraction technique that exploits the flexible granularity of modern reachability analysis algorithms.

For more information, please contact Sergiy Bogomolov

Download here.


SpaceEx with Assume-Guarantee Abstraction Refinement

Merging locations to accelerate reachabilitySpaceEx with assume-guarantee reasoning support allows for the compositional analysis of large systems consisting of multiple components. In order to build assumptions we introduce an appropriate abstraction based on location merging. We integrate the assume-guarantee style analysis with automatic abstraction refinement.

For more information, please contact Sergiy Bogomolov or Marius Greitschus

Download here.