SciCADE 2011 - Minisymposia

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 VNODE-LP 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 VNODE-LP: 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 VNODE-LP 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 peer-review process. This talk provides an overview of numerical methods behind VNODE-LP, 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 well-known non-injective 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 long-term motion of Near Earth Objects and the verified identification of impact occurrence. In particular, these techniques are applied starting from a simple two-body problem up to a n-body 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.