Third Party Developments and Links
University of Freiburg
SpaceEx with Guided Search
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.
SpaceEx with Assume-Guarantee Abstraction Refinement
SpaceEx 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.
