Analysis of Scientific-Computation Methods
==========================================

The work examines the possibility of using formal-verification methods
and tools for reasoning about scientific-computation methods. The need
to verify about infinite-state systems has led to the development of
formal frameworks for modeling infinite on-going behaviors, and it
seems very likely that these frameworks can also be helpful in the
context of numerical methods. In particular, the use of hybrid
systems, which model infinite-state systems with a finite control,
seems promising.

The work introduces probabilistic o-minimal hybrid systems, which
combine flows definable in an o-minimal structure with the
probabilistic choices allowed in probabilistic hybrid systems.
We show that probabilistic o-minimal hybrid systems have finite
bisimulations, thus the reachability and the nonemptiness problems for
them are decidable.  To the best of our knowledge, this forms the
strongest type of hybrid systems for which the nonemptiness problem is
decidable, hence also the strongest candidate for modelling
scientific-computation methods.