
MINISYMPOSIA 
Validated
Integration Methods for ODEs, II
Organized by
Markus Neher, Karlsruhe Institute of Technology, Germany

Validated integration methods for ODEs aim at computing rigorous
bounds for specific solutions of ODEs. Interval arithmetic has been
used for almost 50 years for this purpose. Recently, Taylor model methods
for ODEs have been developed by Berz and Makino by combining interval
arithmetic with computer algebra. Taylor models reduce the dependency
problem and the wrapping effect intrinsic to interval arithmetic. They
also benefit from their capability of representing nonconvex sets, which
is especially advantageous for enclosing the flows of nonlinear ODEs.
The talks in the minisymosium report on recent developments in validated
methods for ODEs, including applications to practical problems.
SPEAKERS 

Ned
Nedialkov,
McMaster University, Hamilton, Ontario.

An
interval method for ODEs, the VNODELP solver, and literate programming
Interval numerical methods produce rigorous bounds that are guaranteed
to contain mathematically correct solutions. Such bounds are typically
used to ensure that critical calculations are accurate and reliable
by proving that a solution is within certain bounds. However, an
error in the implementation of such a method may invalidate its
rigor.
N.
Nedialkov is the author of VNODELP: a C++ package for computing
rigorous bounds in IVPs for ODEs. A distinctive feature of this
solver is that it is developed entirely using Literate Programming
the theory, documentation, and source code of VNODELP are interwoven
in a single document from which the source code is extracted.
As a result, the correctness of the implementation can be certified
by human experts, by reviewing its LP document, similarly to how
a scientific work is examined for correctness in a peerreview
process.
This
talk provides an overview of numerical methods behind VNODELP,
its capabilities, and implementation. It also presents the author's
experience using literate programming for producing verifiable
numerical software.

Wayne
Hayes
University of California, Irvine

Tinkerbell is Chaotic
Shadowing
is a method of backward error analysis that plays a important
role in hyperbolic dynamics. In this paper, the shadowing by containment
framework is revisited, including a new shadowing theorem. This
new theorem has several advantages with respect to
existing shadowing theorems: it does not require injectivity or
differentiability, and its hypothesis can be easily verified using
interval arithmetic. As an application of this new theorem, shadowing
by containment is shown to be applicable to infinite length orbits
and is used to provide a computer assisted proof of the presence
of chaos in the wellknown noninjective Tinkerbell map.

Pierluigi
Di Lizia,
Politecnico di Milano, Italy

Rigorous
Integration of Asteroid Orbits
Taylor model integrators have recently shown to be a powerful tool
for the validated integration of ordinary differential equations.
By representing the flow of a differential equation by Taylor models
a tight enclosure for the action of the differential equations on
an extended region for a time step $\Delta t$ is provided. Consequently,
the integrated initial conditions can be either point vectors expressed
by real numbers or interval boxes. Thus, either point or interval
initial conditions can be rigorously integrated, so allowing the
propagation of uncertainty boxes on initial conditions.
In
this work the previous feature is exploited to rigorously predict
the longterm motion of Near Earth Objects and the verified identification
of impact occurrence. In particular, these techniques are applied
starting from a simple twobody problem up to a nbody dynamics
including also relevant nongravitational perturbations. In such
a way the validated integration of the motion of significant asteroids
can be addressed considering initial uncertainties consistent
with the current measurement accuracies.
Simple
test cases that show how Taylor model based integration outperforms
classical interval schemes are presented as well as a detailed
analysis of Apophis 2029 close encounter. In the latter case,
the beneficial effects of including both an automatic box splitting
technique and a suitable description of the vector field are analyzed.

