Formal analysis of scientific-computation methods

Abstract

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 frame works for modeling infinite on-going behaviors, and it seems very likely that these frameworks ran 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. srems promising. The work introduces Probabilistic o-mimmal hybrid systems, which combine Hows 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 hisimulatious. thus the reachability and the nonemptiness problems for them are dccidable. To the best, of uur 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.