ISBN 978-3-8439-1625-7

978-3-8439-1625-7, Reihe Informatik

Stefan Kiel
UniVerMeC – A Framework for Development, Assessment and Interoperable Use of Verified Techniques

223 Seiten, Dissertation Universität Duisburg-Essen (2014), Softcover, A5

Zusammenfassung / Abstract

Verified algorithms play an important role in the context of different applications from various areas of science. An open question is the interoperability between different verified range arithmetics and their numerical comparability. In this thesis, a theoretical framework is provided for interoperable handling of the arithmetics without altering their verification features. For this purpose, we formalize the arithmetics using a heterogeneous algebra. Based on this algebra, we introduce the concept of function representation objects. They characterize a mathematical function by inclusion functions in different arithmetics and allow for representing particular features of the function (e.g., differentiability). The representation objects allow us to describe problems by functional and relational dependencies so that different verified methods can be used interchangeably. On this basis, we develop a new verified distance computation algorithm which can handle non-convex objects. Furthermore, a verified global optimization algorithm is adapted so that it can use the different methods made accessible by the function representation objects. Moreover, we formalize and improve interval-based hierarchical structures which are used by both algorithms. To evaluate our approach, we provide a prototypical implementation and perform fair numerical comparisons between the different arithmetics. Finally, we apply the framework to relevant application cases from biomechanics and modeling, simulation and control of fuel cells. We demonstrate that our implementation supports parallel computations on the CPU and GPU and show that it can be extended by interfacing additional external IVP solver libraries.