Talks and Poster Presentations (with Proceedings-Entry):
S. Bogomolov, G. Frehse, R. Grosu, H. Ladan, A. Podelski:
"A Box-Based Distance between Regions for Guiding the Reachability Analysis of SpaceEx";
Talk: CAV'12, the 24th International Conference on Computer Aided Verification,
Berkeley, California, USA;
- 2012-07-13; in: "Proceedings of CAV'12, the 24th International Conference on Computer Aided Verification",
LNCS / Springer,
A recent technique used in falsification methods for hybrid systems relies on distance-based heuristics for guiding the search towards a goal state. The question is whether the technique can be carried over to reachability analyses that use regions as their basic data structure. In this paper, we introduce a box-based distance measure between regions. We present an algorithm that, given two regions, efficiently computes the box-based distance between them. We have implemented the algorithm in SpaceEx and use it for guiding the region-based reachability analysis of SpaceEx. We illustrate the practical potential of our approach in a case study for the navigation benchmark.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
Electronic version of the publication:
Created from the Publication Database of the Vienna University of Technology.