eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
31
10.4230/DagSemProc.08021.1
article
08021 Abstracts Collection – Numerical Validation in Current Hardware Architectures
Luther, Wolfram
Cuyt, Annie
Krämer, Walter
Markstein, Peter
From 06.01. to 11.01.2008, the Dagstuhl Seminar 08021 ``Numerical Validation in Current Hardware Architectures'' was held in the International Conference and Research Center (IBFI), Schloss Dagstuhl.
During the seminar, several participants presented their current
research, and ongoing work and open problems were discussed. Abstracts of
the presentations given during the seminar as well as abstracts of
seminar results and ideas are put together in this paper. The first section
describes the seminar topics and goals in general.
Links to extended abstracts or full papers are provided, if available.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.1/DagSemProc.08021.1.pdf
Computer arithmetic
arbitrary precision
floating-point arithmetic standardization
language support
reliable libraries,high-precision special functions
reliablealgorithms
reliable floating-point and interval computing on different platforms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
0
10.4230/DagSemProc.08021.2
article
08021 Summary – Numerical Validation in Current Hardware Architectures
Cuyt, Annie
Krämer, Walter
Luther, Wolfram
Markstein, Peter
Numerical validation in current hardware architectures - From embedded system to high-end computational grids
Topics
List of participants
Schedule
List of talks
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.2/DagSemProc.08021.2.pdf
Computer arithmetic
arbitrary precision
floating-point arithmetic standardization
language support
reliable libraries
high-precision special functions
reliablealgorithms
reliable floating-point and interval computing on different platforms
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
23
10.4230/DagSemProc.08021.3
article
A Modified Staggered Correction Arithmetic with Enhanced Accuracy and Very Wide Exponent Range
Blomquist, Frithjof
Hofschuster, Werner
Krämer, Walter
A so called staggered precision arithmetic is a special kind of
a multiple precision arithmetic based on the underlying
floating point data format (typically IEEE double format)
and fast floating point operations as well as exact dot product computations.
Due to floating point limitations it is not an arbitrary precision arithmetic.
However, it typically allows computations using several hundred mantissa digits.
A set of new modified staggered arithmetics for real and
complex data as well as for real interval and
complex interval data with very wide exponent range is presented.
Some applications show
the increased accuracy of computed results compared to ordinary staggered
interval computations. The very wide exponent range of the new arithmetic
operations allows computations far beyond the IEEE data formats.
The new arithmetics would be extremly fast, if an exact dot product was
available in hardware (the fused accumulate and add instruction is only
one step in this direction).
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.3/DagSemProc.08021.3.pdf
Staggered correction
multiple precision
C-XSC
interval computation
wide exponent range
reliable numerical computations
complex interval funct
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
14
10.4230/DagSemProc.08021.4
article
A Note on Solving Problem 7 of the SIAM 100-Digit Challenge Using C-XSC
Kolberg, Mariana
Krämer, Walter
Zimmer, Michael
C-XSC is a powerful C++ class library which simplifies the development
of selfverifying numerical software. But C-XSC is not only a development tool, it also provides a lot of predefined highly accurate routines to compute reliable bounds for the solution to standard numerical problems.
In this note we discuss the usage of a reliable linear system solver to compute the solution of problem 7 of the SIAM 100-digit challenge. To get the result we have to solve a 20 000 Ãƒâ€” 20 000 system of linear equations using interval computations. To perform this task we run our software on the advanced Linux cluster engine ALiCEnext located at the University of Wuppertal and on the high performance computer HP XC6000 at the computing center of the University of Karlsruhe.
The main purpose of this note is to demonstrate the power/weakness of our approach to solve linear interval systems with a large dense system matrix using C-XSC and to get feedback from other research groups all over the world concerned with the topic described. We are very much interested to see comparisons concerning different methods/algorithms, timings, memory consumptions, and different hardware/software
environments. It should be easy to adapt our main routine (see Section 3 below) to other programming languages, and different computing environments. Changing just one variable allows the generation of arbitrary large system matrices making it easy to do sound (reproducible and comparable) timings and to check for the largest possible system size that can be handled successfully by a specific package/environment.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.4/DagSemProc.08021.4.pdf
C-XSC
reliable computing
100-digit challenge
reliable linear system solver
high performance computing
large dense linear systems
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
4
10.4230/DagSemProc.08021.5
article
A Note on Some Applications of Interval Arithmetic in Hierarchical Solid Modeling
Dyllong, Eva
Techniques of reliable computing like interval arithmetic can be used to
guarantee a reliable solution even in the presence of numerical round-off
errors. The need to trace bounds for the error function separately can be
eliminated using these techniques. In this talk, we focus on some
demonstrations how the techniques and algorithms of reliable computing
can be applied to the construction and further processing of hierarchical
solid representations using the octree model as an example.
An octree is a common hierarchical data structure to represent 3D
geometrical objects in solid modeling systems or to reconstruct a real
scene. The solid representation is based on recursive cell decompositions
of the space. Unfortunately, the data structure may require a large amount
of memory when it uses a set of very small cubic nodes to approximate a
solid.
In this talk, we present a novel generalization of the octree model created
from a CSG object that uses interval arithmetic and allows us to extend the
tests for classifying points in space as inside, on the boundary or outside
the object to handle whole sections of the space at once. Tree nodes with
additional information about relevant parts of the CSG object are
introduced in order to reduce the depth of the required subdivision.
Furthermore, this talk is concerned with interval-based algorithms for
reliable proximity queries between the extended octrees and with further
processing of the structure. We conclude the talk with some examples of
implementations.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.5/DagSemProc.08021.5.pdf
Reliable solid modeling
hierarchical data structure
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
3
10.4230/DagSemProc.08021.6
article
A Software Library for Reliable Online-Arithmetic with Rational Numbers
de Miguel Casado, Gregorio
García Chamizo, Juan Manuel
An overview of a novel calculation framework for scientific computing in integrable spaces is introduced. This paper discusses some
implementation issues adopted for a software library devoted to exact rational
online-arithmetic operators for periodic rational operands codified in fractional positional notation.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.6/DagSemProc.08021.6.pdf
Computable analysis
online-arithmetic
rational numbers
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
4
10.4230/DagSemProc.08021.7
article
C-XSC and Closely Related Software Packages
Hofschuster, Werner
Krämer, Walter
Neher, Markus
C-XSC and Closely Related Software Packages
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.7/DagSemProc.08021.7.pdf
Mathematical software
reliable computing
C-XSC
CoStLy
ACETAF
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
12
10.4230/DagSemProc.08021.8
article
Complete Interval Arithmetic and its Implementation
Kulisch, Ulrich
A Complete Interval Arithmetic and its Implementation is discussed.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.8/DagSemProc.08021.8.pdf
Interval Arithmetic
implementation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
14
10.4230/DagSemProc.08021.9
article
Distributed parameter and state estimation in a network of sensors
Kieffer, Michel
In this paper, we have considered distributed bounded-error state estimation applied to the problem of source tracking with a network of wireless sensors. Estimation is performed in a distributed context, emph{i.e.}, each sensor has only a limited amount of measurements available. A guaranteed set estimator is put at work. At each time instant, any sensor of the node has its own set estimate of the location of the source.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.9/DagSemProc.08021.9.pdf
Parameter estimation
state estimation
bounded errors
nonlinear estimation
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
14
10.4230/DagSemProc.08021.10
article
Extending the Range of C-XSC: Some Tools and Applications for the use in Parallel and other Environments
Grimmer, Markus
There is a broad range of packages and libraries for verified numerical
computation. C-XSC is a library combining one of the most extensive
sets of functions and operations on the one hand with a wide range of
applications and special features on the other hand. As such it is an
important task both to make use of its existing capabilities in applications
and to develop further extensions giving access to additional areas and
environments.
In this talk, we present some examples of extensions for C-XSC that
have been developed lately. Among these are extensions that give access
to further hardware and software environments as well as applications
making use of these possibilities.
Software libraries for interval computation always imply great computation
effort: One way to reduce computation times is the development
of parallel methods to make use of parallel hardware. For this, it is important
that the features and data types of the used library can be easily
used in parallel programs. An MPI package for C-XSC data types allows
to easily use C-XSC in parallel programs without bothering about the internal
structure of data types. Another extension of C-XSC, the C-XSC
Taylor arithmetic, is also covered by the MPI package. Parallel verified
linear system solvers based on the package are available as well, and further
development has been and is being done to integrate more efficient
methods for interval linear system solution.
One application making use of the mentioned extensions is a parallel
verified Fredholm integral equation solver. Some results are given to
demonstrate the reduction of computation time and, at the same time,
the accuracy gain that can be obtained using the increased computation
power. Naturally, hardware interval support would offer still more
possibilities towards optimal performance of verified numerical software.
Another possibility to extend the range of C-XSC is to make results
available for further computations in other software environments as,
for example, computer algebra packages. An example of this is presented
for the Maple interval package intpakX. This kind of interfaces also
allows the user to get access to further platforms like operating systems,
compilers or even hardware.
References:
[1] ALiCEnext: http://www.alicenext.uni-wuppertal.de.
[2] Blomquist, F.; Hofschuster, W.; Kraemer, W.: Real and Complex Taylor
Arithmetic in C-XSC. Preprint BUW-WRSWT 2005/4, University of
Wuppertal, 2005.
[3] Grimmer, M.; Kraemer, W.: An MPI Extension for Verified Numerical Computations
in Parallel Environments. In: Int. Conf. on Scientific Computing
(CSC’07, Worldcomp’07) Las Vegas, June 25-28, 2007, Proceedings
pp. 111-117, Arabnia et al. (eds.), 2007.
[4] Grimmer, M.: An MPI Extension for the Use of C-XSC in Parallel Environments.
Preprint BUW-WRSWT 2005/3, University of Wuppertal,
2005.
[5] Grimmer, M.: Selbstverifizierende mathematische Softwarewerkzeuge im
High Performance Computing. Dissertation, Logos Verlag, Berlin, 2007.
[6] Grimmer, M.: Interval Arithmetic in Maple with intpakX. In: PAMM -
Proceedings in Applied Mathematics and Mechanics, Vol. 2, Nr. 1, p.
442-443, Wiley-InterScience, 2003.
[7] Hofschuster, W.; Kraemer, W.: C-XSC 2.0: A C++ Library for Extended
Scientific Computing. Numerical Software with Result Verification, Lecture
Notes in Computer Science, Volume 2991/2004, Springer-Verlag, Heidelberg,
pp. 15 - 35, 2004.
[8] Klein, W.: Enclosure Methods for Linear and Nonlinear Systems of Fredholm
Integral Equations of the Second Kind. In: Adams, Kulisch: Scientific
Computing with Result Verification, Academic Press, 1993.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.10/DagSemProc.08021.10.pdf
C-XSC
Integral Equations
Interval Arithmetic
Maple
MPI
Parallel Environment
Taylor Arithmetic
Verified Linear System Solver.
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
20
10.4230/DagSemProc.08021.11
article
Fast (Parallel) Dense Linear Interval Systems Solvers in C-XSC Using Error Free Transformations and BLAS
Zimmer, Michael
Krämer, Walter
The traditional solver for linear interval systems available in C-XSC [6,1]
is mathematically based on the Krawczyk[12] operator and modifications
introduced by Rump[17]. The Krawczyk operator is composed of
matrix/vector operations. These operations are realized in C-XSC
with higest accuracy (only one final rounding) using a so called long
accumulator (dotprecision variable). C-XSC dotprecision variables allow the
error free computation of sums of floating point numbers as well as the
error free computation of scalar products of floating point vectors. Thus,
from a mathematical point of view these operations are perfect. Because
actual hardware does not support these perfect scalar products all
operations have to be realized by software. This fact leads to a tremendous
time penalty (note: it has been shown that with modest additional hardware
costs perfect scalar products can be made as fast as simple floating-point
loops).
To speed up the C-XSC scalar product software-operations we adapt the so
called DotK algorithm as published in [14]. Error free transformations[14,3,4,10]
are used as basic building blocks to develop summation and scalar product
algorithms simulating a K-fold precision. Compared to the perfect C-XSC operations
these operations are fast. They are more accurate than simple floating-point
loops (but of course no longer perfect in the mathematical sense). The fast
operations are available in C-XSC via the new data types DotK, IDotK, CDotk
and CIDotK. These new data types are composed in such a way that traditional
C-XSC code using dotprecision variables can be adapted with minimal effort. It is
possible to switch (at runtime!) from perfect computations to fast operations using
K-fold precision (K equal 0 means traditional dotprecision computations) and it is
possible to hold intermediate results with corresponding error bounds for further
summations or scalar product updates. The details are described in [19].
Additionaly, based on similar algorithms used in Intlab[16], BLAS and LAPACK
libraries [2] are used in the O(nÃ‚Â³) parts of the linear system solver. For
matrix-matrix products, manipulation of the rounding mode of the processor is used
to compute enclosures of the correct result.
Comparing the traditional solver with the new version shows that the class of
problems which are solvable with the new version is smaller than the class of
problems which can be solved using the solver based on perfect operations. But it
seems that for real world problems also the new solver is appropriate. Using the
new solver based on BLAS and simulating a quadrupel precision (i.e. k==2) the
speedup comes close to 200(!). The new solver is nearly as fast as the corresponding
IntLab[16] solver verifylss. Solving a real linaer system of dimension 1000 on a
Pentium 4 with 3.2GHz takes about 2.8 seconds. In all cases tested the accuracy of
our new solver was better and in some cases significantly better than the accuracy
of the corresponding IntLab results. The new solver also allows solving larger
(dense) problems than its IntLab counterpart. We also show some examples where IntLab
falls down whereas our new solver still works.
A parallel version of this solver, based on ScaLAPACK, is also available. Unlike
the previous parallel solver in C-XSC[5], this new solver does not depend on a
root-node, which makes it possible to compute a verified solution even of very large
linear systems.
In the talk we will discuss the new data types in more detail, we will emphasize our
modifications to the DotK algorithm taken from the literature [14,15], we will show
time measurements and we will present results concerning the accuracy of the computed
enclosures. Our results will also be compared to corresponding results computed with
the IntLab package. We also will comment on hardware features and compiler options
which can/should be used to get reliable results on different platforms efficiently.
References:
[1] Downloads:
C-XSC library: http://www.math.uni-wuppertal.de/~xsc/xsc/cxsc.html
Solvers: http://www.math.uni-wuppertal.de/~xsc/xsc/cxsc_software.html
[2] L.S. Blackford, J. Demmel, J. Dongarra, I. Duff, S. Hammarling, G. Henry, M. Heroux,
L. Kaufman, A. Lumsdaine, A. Petitet, R. Pozo, K. Remington, R. C. Whaley, An Updated Set
of Basic Linear Algebra Subprograms (BLAS), ACM Trans. Math. Soft., 28-2 (2002), pp. 135--151.
[3] Bohlender, G.; Walter, W.; Kornerup, P.; Matula,
D.W.; Kornerup, P.; Matula, D.W.:
Semantics for Exact Floating Point Operations.
Proceedings, 10th IEEE Symposium on Computer Arithmetic,
26-28 June 1991, IEEE, 1991.
[4] Dekker, T.J.: A floating-point technique for extending
the available precision. Numer. Math., 18:224, 1971.
[5] Grimmer, M.: Selbstverifizierende Mathematische Softwarewerkzeuge im
High-Performance Computing. Konzeption, Entwicklung und Analyse am Beispiel
der parallelen verifizierten Loesung linearer Fredholmscher Integralgleichungen
zweiter Art. Logos Verlag, 2007.
[6] Hofschuster, W.; Kraemer, W.:
C-XSC 2.0: A C++ Library for Extended Scientific Computing.
Numerical Software with Result Verification,
Lecture Notes in Computer Science, Volume 2991/2004,
Springer-Verlag, Heidelberg, pp. 15 - 35, 2004.
[7] Kersten, Tim: Verifizierende rechnerinvariante Numerikmodule, Dissertation,
University of Karlsruhe, 1998
[8] Klatte, Kulisch, Wiethoff, Lawo, Rauch:
"C-XSC - A C++ Class Library for Extended Scientific Computing",
Springer-Verlag, Heidelberg, 1993.
Due to the C++ standardization (1998) and dramatic changes
in C++ compilers over the last years this documentation describes
no longer the actual C-XSC environment. Please refer to more accurate
documentation (e.g.[1]) available from the web site of our
research group: http...
[9] Kirchner, R., Kulisch, U.:
Hardware Support for Interval Arithmetic.
Reliable Computing, Volume 12, Number 3,
June 2006 , pp. 225-237(13).
[10] Knuth, D.E.: The Art of Computer Programming: Seminumerical Algorithms.
Addison Wesley, 1969, vol. 2.
[11] Kulisch, U.: Computer Arithmetic and Validity - Theory,
Implementation. To appear.
[12] Krawczyk, R.: Newton-Algorithmen zur Bestimmung von Nullstellen mit Fehlerschranken,
Computing, 4:187-201, 1969.
[13] Lerch, M.; Tischler, G.; Wolff von Gudenberg, J.; Hofschuster, W;
Kraemer, W.:
filib++, a Fast Interval Library Supporting Containment Computations.
ACM TOMS, volume 32, number 2, pp. 299-324, 2006.
[14] Ogita, T., Rump, S.M., Oishi, S.: Accurate sum and
dot product. SIAM Journal on Scientific Computing,
26:6, 2005.
[15] Oishi, S., Tanabe, K., Ogita, T., Rump, S.M., Yamanaka, N.:
A Parallel Algorithm of Accurate Dot Product.
Submitted for publication, 2007.
[16] Rump, S.M.: Intlab - Interval Laboratory. Developments in Reliable
Computing, pp. 77-104, 1999.
[17] Rump, S.M.: Kleine Fehlerschranken bei Matrixproblemen, Dissertation,
University of Karlsruhe, 1980
[18] Stroustrup, Bjarne: The C++-Programming Language, 3rd Edition, Addison-Wesley, 2000.
[19] Zimmer, Michael: Laufzeiteffiziente, parallele Loeser fuer
lineare Intervallgleichungssysteme in C-XSC, Master thesis,
University of Wuppertal, 2007.
AMS subject classification: 65H10, 15-04, 65G99, 65G10, 65-04
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.11/DagSemProc.08021.11.pdf
Error-free transformations
K-fold accuracy
accurate dot product
C-XSC
high accuracy
dense linear systems
verified computation.
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
3
10.4230/DagSemProc.08021.12
article
Implementation of the reciprocal square root in MPFR
Zimmermann, Paul
We describe the implementation of the reciprocal square root --- also called
inverse square root --- as a native function
in the MPFR library. The difficulty is to implement
Newton's iteration for the reciprocal square root on top's of GNU MP's
extsc{mpn} layer, while guaranteeing a rigorous $1/2$ ulp bound on the
roundoff error.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.12/DagSemProc.08021.12.pdf
Multiple precision
floating-point
inverse square root
correct rounding
MPFR library
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
5
10.4230/DagSemProc.08021.13
article
Improving the Performance of a Verified Linear System Solver Using Optimized Libraries and Parallel Computation
Kolberg, Mariana
Bohlender, Gerd
Claudio, Dalcidio
A parallel version of the self-verified method for solving linear systems
was presented on PARA and VECPAR conferences in 2006. In this research we propose improvements aiming
at a better performance. The idea is to implement an algorithm that uses technologies
as MPI communication primitives associated to libraries as LAPACK,
BLAS and C-XSC, aiming to provide both self-verification and speed-up at the
same time. The algorithms should find an enclosure even for very ill-conditioned
problems. In this scenario, a parallel version of a self-verified solver for dense
linear systems appears to be essential in order to solve bigger problems. Moreover,
the major goal of this research is to provide a free, fast, reliable and accurate
solver for dense linear systems.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.13/DagSemProc.08021.13.pdf
Linear systems
result verification
parallel computing
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
14
10.4230/DagSemProc.08021.14
article
Interval Arithmetic and Standardization
Wolff von Gudenberg, Jürgen
Interval arithmetic is arithmetic for continuous sets. Floating-point intervals are intervals of real numbers with floating-point bounds.
Operations for intervals can be efficiently implemented. There is an unanimous agreement, how to define the basic operations,
if we exclude division by an interval containing zero. Hence, it should be standardized.
For division by zero, two options are possible, the clean exception free interval arithmetic or the containment arithmetic.
They can be standardized as options.
Elementary functions for intervals can be defined. In some application areas loose evaluation of functions,
i.e. evaluation over an interval which is not completely contained in the function domain, is recommended,
In this case, however, a discontinuity flag has to be set to inform that Brouwer's fixed point theorem is no longer applicable in that case.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.14/DagSemProc.08021.14.pdf
Intervals
containment sets
IEEE754r
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
15
10.4230/DagSemProc.08021.15
article
Numerical Verification Assessment in Computational Biomechanics
Auer, Ekaterina
Luther, Wolfram
In this paper, we present several aspects of the recent project PROREOP, in which a new prognosis system is developed for optimizing patient-specific preoperative surgical planning for the human skeletal system. We address verification and validation assessment in PROREOP with special emphasis on numerical accuracy and performance. To assess numerical accuracy, we propose to employ graded instruments, including accuracy tests and error analysis. The use of such instruments is exemplified for the process of accurate femur reconstruction. Moreover, we show how to verify the simulation results and take into account measurement uncertainties for a part of this process using tools and techniques developed in the project TellHIM&S.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.15/DagSemProc.08021.15.pdf
Numerical verification assessment
validation
uncertainty
result verification
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
13
10.4230/DagSemProc.08021.16
article
On the Interoperability between Interval Software
Popova, Evgenija D.
The increased appreciation of interval analysis as a powerful tool for controlling round-off errors and modelling
with uncertain data leads to a growing number of diverse interval software. Beside in some other aspects,
the available interval software differs with respect to the environment in which it operates and the provided
functionality. Some specific software tools are built on the top of other more general interval software but
there is no single environment supporting all (or most) of the available interval methods. On another side,
most recent interval applications require a combination of diverse methods. It is difficult for the end-users
to combine and manage the diversity of interval software tools, packages, and research codes, even the latter
being accessible. Two recent initiatives: [1], directed toward developing of a comprehensive full-featured library
of validated routines, and [3] intending to provide a general service framework for validated computing in
heterogeneous environment, reflect the realized necessity for an integration of the available methods and
software tools.
It is commonly understood that quality comprehensive libraries are not compiled by a single person or small
group of people over a short time [1]. Therefore, in this work we present an alternative approach based on
interval software interoperability.
While the simplest form of interoperability is the exchange of data files, we will focus on the ability to run
a particular routine executable in one environment from within another software environment, and vice-versa,
via communication protocols. We discuss the motivation, advantages and some problems that may appear in
providing interoperability between the existing interval software.
Since the general-purpose environments for scientific/technical computing like Matlab, Mathematica, Maple, etc.
have several features not attributable to the compiled languages from one side and on another side most problem
solving tools are developed in some compiled language for efficiency reasons, it is interesting to study
the possibilities for interoperability between these two kinds of interval supporting environments.
More specifically, we base our presentation on the interoperability between Mathematica [5] and external
C-XSC programs [2] via MathLink communication protocol [4]. First, we discuss the portability and reliability
of interval arithmetic in Mathematica. Then, we present MathLink technology for building external
MathLink-compatible programs. On the example of a C-XSC function for solving parametric linear systems,
called from within a Mathematica session, we demonstrate some advantages of interval software interoperability.
Namely, expanded functionality for both environments, exchanging data without using intermediate files and
without any conversion but under dynamics and interactivity in the communication, symbolic manipulation interfaces
for the compiled language software that often make access to the external functionality from within Mathematica
more convenient even than from its own native environment. Once established, MathLink connection to external
interval libraries or problem-solving software opens up an array on new possibilities for the latter.
References:
[1] G. Corliss, R. B. Kearfott, N. Nedialkov, S. Smith: Towards an Interval Subroutine Library,
Workshop on Reliable Engineering Computing, Svannah, Georgia, USA, Feb. 22-24, 2006.
[2] W. Hofschuster: C-XSC: Highlights and new developments. In: Numerical Validation in Current Hardware
Architectures. Number 08021 Dagstuhl Seminar, Internationales Begegnungs- und Forschungszentrum f"ur
Informatik, Schloss Dagstuhl, Germany, 2008.
[3] W. Luther, W. Kramer: Accurate Grid Computing, 12th GAMM-IMACS Int. Symposium on Scientific Computing,
Computer Arithmetic and Validated Numerics (SCAN 2006), Duisburg, Sept. 26-29, 2006.
[4] Ch. Miyaji, P. Abbot eds.: Mathlink: Network Programming with Mathematica, Cambridge Univ. Press, Cambridge, 2001.
[5] Wolfram Research Inc.: Mathematica, Version 5.2, Champaign, IL, 2005.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.16/DagSemProc.08021.16.pdf
Software interoperability
interfacing
interval software
C-XSC
MathLink
Mathematica
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
10
10.4230/DagSemProc.08021.17
article
Robustness of Boolean operations on subdivision-surface models
Jiang, Di
Stewart, Neil
This work was presented in two parts at Dagstuhl seminar 08021.
The two presentations described work in
progress, including a ``backward bound'' for a combined backward/forward
error analysis for the problem mentioned in the title.
We seek rigorous proofs that representations of computed sets, produced by
algorithms to compute Boolean operations, are well formed, and that the
algorithms are correct. Such proofs should eventually take account of the use of
finite-precision arithmetic, although the proofs presented here do not.
The representations studied are based on subdivision surfaces. Such
representations are being used more and more frequently in place of trimmed
NURBS representations, and the robustness analysis for these new representations
is simpler than for trimmed NURBS.
The particular subdivision-surface representation used is based on the Loop
subdivision scheme. The analysis is broken into three parts. First, it is
established that the input operands are well-formed two-dimensional manifolds
without boundary. This can be done with existing methods.
Secondly, we introduce the so-called ``limit mesh'', and view the
limit meshes corresponding to the input sets as defining an approximate problem
in the sense of a backward error analysis. The presentations mentioned above
described a proof of the corresponding error bound. The third part of the
analysis corresponds to the ``forward bound'': this remains to be done.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.17/DagSemProc.08021.17.pdf
Robustness
finite-precision arithmetic
Boolean operations
subdivision surfaces
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
8
10.4230/DagSemProc.08021.18
article
Second Note on Basic Interval Arithmetic for IEEE754R
Pryce, John D.
Corliss, George C.
Kearfott, R. Baker
Nedialkov, Ned S.
Smith, Spencer
The IFIP Working Group 2.5 on Numerical Software (IFIPWG2.5) wrote on 5th Septem-
ber 2007 to the IEEE Standards Committee concerned with revising the IEEE Floating-
Point Arithmetic Standards 754 and 854 (IEEE754R), expressing the unanimous
request of IFIPWG2.5 that the following requirement be included in the future computer
arithmetic standard:
For the data format double precision, interval arithmetic should be made
available at the speed of simple floating-point arithmetic.
IEEE754R (we believe) welcomed this development. They had before them a document
defining interval arithmetic operations but, to be the basis of a standards document, it
needed more detail. Members of the Interval Subroutine Library (ISL) team were asked
to comment, in an email from Ulrich Kulisch that enclosed one from Jim Demmel to Van
Snyder raising the issue. This paper provides ISL's comments.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.18/DagSemProc.08021.18.pdf
Interval arithmetic
validated computation
floating point
standards
exceptions
not an interval
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
6
10.4230/DagSemProc.08021.19
article
The CoStLy C++ Class Library
Neher, Markus
CoStLy (ul{Co}mplex ul{St}andard Functions ul{L}ibrarul{y}) has been
developed as a C++ class library for the validated computation of function
values and of ranges of complex standard functions. If performed in exact arithmetic, the inclusion functions for principal branches compute
optimal range bounds. For the sake of accuracy, a major effort has been made in the implementation of the algorithms in floating point arithmetic to eliminate all intermediate expressions subject to numerical overflow, underflow, or cancellation. The CoStLy library has been extensively tested for arguments with absolute values ranging from 1.0E-300 to 1.0E+300. For most arguments, the computed bounds for function values are highly accurate. In many test cases, the observed precision of the result was about 50 correct bits (out of the 53 bits available in IEEE 754 floating point arithmetic) for point arguments.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.19/DagSemProc.08021.19.pdf
Complex interval arithmetic
inclusion functions
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
3
10.4230/DagSemProc.08021.20
article
The New IEEE-754 Standard for Floating Point Arithmetic
Markstein, Peter
The current IEEE-754 floating point standard
was adopted 23 years ago. IEEE chartered a committee to
revise the standard to include new common practice in
floating point arithmetic, to incorporate decimal floating
point into the standard, and to address the issue of
reproducible results. This talk will visit these issues,
based on the current work of the IEEE-754 revisions
committee, which expects that a new standard will be
adopted sometime in 2008.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.20/DagSemProc.08021.20.pdf
Floating point arithmetic
standards
eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Dagstuhl Seminar Proceedings
1862-4405
2008-04-22
8021
1
10
10.4230/DagSemProc.08021.21
article
Towards the Development of an Interval Arithmetic Environment for Validated Computer-Aided Design and Verification of Systems in Control Engineering
Rauh, Andreas
Minisini, Johanna
Hofer, Eberhard P.
Modern techniques for the design and analysis of control strategies for nonlinear dynamical systems are often based on the simulation of the open-loop as well as the closed-loop dynamical behavior of suitable mathematical models. In control engineering, continuous-time and discrete-time state-space representations are widely used which are given by sets of ordinary differential equations and difference equations, respectively. In addition to these representations, sets of differential algebraic equations are commonly used. Since we will focus on computational techniques which are applied for the design and mathematical verification of controllers for lumped parameter systems, i.e., systems which do not contain elements with distributed parameters, partial differential equations will not be considered in this talk.
The prerequisite for the design and robustness analysis of each control system is the identification of mathematical models which describe the dynamics of the plant to be controlled as well as the available measurement devices with a sufficient accuracy. The model identification task comprises the derivation of physically motivated state equations, their parameterization based on measured data, as well as simplifications to apply specific approaches for controller design.
In the design stage, both open-loop and closed-loop control strategies can be considered. Since dynamical system models are subject to uncertain parameters and uncertain initial conditions in most practical applications, detailed mathematical formulations of the desired dynamics of the controlled system are necessary. These specifications involve the definition of robustness with respect to the above-mentioned uncertainties. For linear system representations, robustness is commonly specified in terms of regions in the complex domain containing all admissible poles of the closed-loop transfer functions ($Gamma$-stability) or in terms of specifications of worst-case bounds for the frequency response ($mathcal{B}$-stability) [1].
However, these specifications do not allow for inclusion of bounds for the state variables which are often available in the time domain if controllers are designed for safety critical applications. Especially for nonlinear dynamical systems, pole assignment based on the linearization of nonlinear mathematical models generally leads to the necessity for the analysis of asymptotic stability of the resulting closed-loop dynamics.
In this presentation, we will give an overview of the potential use of validated techniques for the analysis and design of controllers for nonlinear dynamical systems with uncertainties, where the systems under consideration will be subject to constraints for both state and control variables.
As an application scenario the design of robust control strategies for a biological wastewater treatment process will be discussed. In the design and the verification process, constraints for both state and control variables which are given by guaranteed interval bounds in the time domain are taken into account. Suitable computational techniques are, for example, based on an extension of the validated initial value problem solver {sc ValEncIA-IVP} [2,6]. For that purpose, differential sensitivities of the trajectories of all state variables with respect to variations of the parameters of the mathematical system model as well as the adaptation of controller parameters are computed. This information can then be used for online identification and adaptation of parameters during the operation of a closed-loop controller as well as in offline design, verification, and optimization. Here, the interval arithmetic routines for sensitivity analysis allow to compute guaranteed differential sensitivity measures for system models with both nominal parameters and interval uncertainties.
The presented interval arithmetic techniques are the basis for a general purpose tool for the analysis and the design of robust and optimal control strategies for uncertain dynamical systems. The presentation is concluded with an outlook on the formulation of control problems using sets of differential algebraic equations. Possibilities for the extension of {sc ValEncIA-IVP} to this type of system representation will be summarized. Relations between the presented interval arithmetic approach and methods for stabilizing control of nonlinear dynamical systems which make use of structural system properties such as differential flatness [3] and exact feedback linearization are highlighted [4,5]. In the latter case, input-output linearization as well as (in special cases) input-to-state linearization are of practical importance.
References:
[1] J. Ackermann, P. Blue, T. B"unte, L. G"uvenc, D. Kaesbauer, M. Kordt, M. Muhler, and D. Odenthal, {it{Robust Control: The Parameter Space Approach}}, Springer--Verlag, London, 2nd edition, 2002.
[2] E. Auer, A. Rauh, E. P. Hofer, and W. Luther, {it{Validated Modeling of Mechanical Systems with {sc SmartMOBILE}: Improvement of Performance by {sc ValEncIA-IVP}}}, In Proceedings of Dagstuhl Seminar 06021: Reliable Implementation of Real Number Algorithms: Theory and Practice, Lecture Notes in Computer Science, Dagstuhl, Germany, 2006. In print.
[3] M. Fliess, J. LÃƒÂ©vine, P. Martin, and P. Rouchon, {it{Flatness and Defect of Nonlinear Systems: Introductory Theory and Examples}}, International Journal of Control, vol. 61, pp. 1327--1361, 1995.
[4] H. K. Khalil, {it{Nonlinear Systems}}, Prentice-Hall, Upper Saddle River, New Jersey, 3rd edition, 2002.
[5] H. J. Marquez, {it{Nonlinear Control Systems}}, John Wiley & Sons, Inc., New Jersey, 2003.
[6] A. Rauh and E. Auer, {{www.valencia-ivp.com}}.
https://drops.dagstuhl.de/storage/16dagstuhl-seminar-proceedings/dsp-vol08021/DagSemProc.08021.21/DagSemProc.08021.21.pdf
Interval techniques
{sc{ValEncIA-IVP}}
controller design
robustness
validated integration of ODEs
parameter uncertainties
sensitivity analysis