Sergiy Bogomolov

Date: 17:00, Thursday, November 28, 2013
Speaker: Sergiy Bogomolov
Venue: IST Austria
Notes:

Hybrid systems represent an important and powerful formalism for
modeling real-world applications such as embedded systems. A
verification tool like SpaceEx is based on the exploration of a
symbolic search space (the region space). As a verification tool, it
is typically optimized towards proving the absence of errors. In some
settings, e.g., when the verification tool is employed in a
feedback-directed design cycle, one would like to have the option to
call a version that is optimized towards finding an error path in the
region space. A recent approach in this direction is based on guided
search. Guided search relies on a cost function that indicates which
states are promising to be explored, and preferably explores more
promising states first. In this talk, we present two approaches to
define and compute efficient cost functions. We develop our approaches
on the top of the symbolic hybrid model checker SpaceEx which uses
regions as its basic data structures.In the first part of the talk, we introduce a box-based distance measure

which is based on the distance between regions in the concrete state space.
In the second part of the talk, we discuss an abstraction-based cost function
based on pattern databases for guiding the reachability analysis.
For this purpose, a suitable abstraction technique that exploits the flexible
granularity of modern reachability analysis algorithms is introduced.
We illustrate the practical potential of our approaches in several case studies.
Posted in RiSE Seminar