[1] Elke Just and Bruno Lang. Success-guided selection of expanded systems for result-verifying nonlinear solvers. Reliab. Comput., 16:73--83, March 2012. [ .pdf ]
Most result-verifying solvers for nonlinear systems include a branch-and-bound algorithmic backbone, complemented with accelerating methods such as Constraint Propagation, Interval Newton, and many others. Often the effectiveness of the accelerators can be improved if one works not only with the given system but also with expanded systems, which are obtained by introducing additional variables for suitable subterms. While reducing the overall number of boxes that must be considered during the solution, applying the accelerators to the (often much larger) expanded systems can increase significantly the time spent on a single box. Therefore a good strategy for deciding which methods to apply to which expanded system is essential for the performance and robustness of the whole solver.

We propose a heuristic that selects expanded systems based on performance information gathered during the computations. Numerical experiments show that this new dynamical strategy tends to be superior to a fixed small-to-large traversal (with restarts) of the expanded systems, which has been the default strategy in our nonlinear solver and optimizer SONIC.

[2] Thomas Beelitz, Bruno Lang, Peer Ueberholz, and Paul Willems. Closing the case t = 3 for 3-D spherical t-designs using a result-verifying nonlinear solver. Reliab. Comput., 14:66--77, June 2010. [ .pdf ]
The question if there exists an N-point spherical t-design is not yet settled for all combinations of t and N. Using our framework SONIC for the solution of nonlinear systems, we were able to close the two remaining open cases for t = 3. More precisely, a computational proof revealed that there are no spherical 3-designs with N = 7 or N = 9 points. We describe how these results were obtained and comment on the open cases for larger values of t.

[3] Thomas Beelitz, Andreas Frommer, Bruno Lang, and Paul Willems. A framework for existence tests based on the topological degree and homotopy. Numer. Math., 111(4):493--507, February 2009. [ DOI ]
The invariance of the topological degree under certain homotopies is used to derive a framework for tests to computationally prove the existence of zeros of nonlinear mappings in Rn. These tests use interval arithmetic to enclose the range of a function over a box and are provably more general than many other tests like the Moore--Kioustelidis test, a test based on the Krawczyk operator, and another degree--based test published recently. A numerical example is included.