vncap
International Workshop on Validated Numerics for Computer-Assisted Proofs
Validated Numerics for Computer-Assisted Proofs
6-10 July 2026, ICMS, Bayes Centre, Edinburgh
Abstracts and Long Programme
Note: The programme is provisional and subject to changes.
Sun 05 Jul 2026
Arrivals and Check-in
Suggested activity
Mon 06 Jul 2026
09:00-10:00 Registration and refreshments
Join us at the ICMS, top floor of the Bayes Centre. Refreshments will be provided.
10:00-10:15 Housekeeping and Welcome
10:15-11:00 The beginnings of validated numerics, in memory of Hans Koch and Oscar Lanford
Jean-Pierre Eckmann - Université de Genève, Switzerland
Although “everybody” might know how this subject evolved, I will try to reconstruct how the early issues and difficulties came up, and how Koch and Lanford (and many others) worked to make this subject a common modern tool in analysis.
11:00-11:30 Coffee
11:30-12:15 Computer-assisted proofs in nonlinear dynamics based on spectral methods
Jan Bouwe van den Berg - Vrije Universiteit Amsterdam, Netherlands
An expository talk about CAPs in nonlinear dynamics based on spectral methods.
12:15-13:00 Rigorous enclosure of Lyapunov exponents of stochastic flows
Hugo Chu - École Polytechnique, France
Rigorously enclosing Lyapunov exponents of stochastic flows is a long-standing and notoriously difficult problem: even determining the sign of the top exponent is often out of reach outside special structures or perturbative regimes. In this paper, we develop a computer-assisted method to obtain rigorous upper and lower bounds on Lyapunov exponents of stochastic flows under mild hypoellipticity assumptions. Our approach starts from the Furstenberg-Khasminskii representation of the top Lyapunov exponent as an ergodic average over the invariant measure of the associated projective process, but crucially avoids any rigorous computation of that invariant measure. Instead, we introduce a numerical adjoint method, amenable to rigorous numerics, and show that an approximate solution of the associated Poisson equation yields a certified enclosure of the Lyapunov exponent via an explicit bound on the residual. This converts a non-rigorous numerical approximation into a rigorous quantitative estimate. The method applies to systems on both compact and non-compact state spaces, does not require special geometric structure, and is not restricted to small-noise or other perturbative settings. We use it to prove positivity of the top Lyapunov exponent for several stochastic systems, including examples exhibiting noise-induced chaos and parameter-dependent sign changes, and we combine it with continuation methods to obtain rigorous bounds over large parameter regions.
13:00-14:00 Lunch
14:00-14:30 (Part I - TBC)
Polina Vytnova - University of Surrey, England
(Pending)
14:30-15:00 (Part II - TBC)
Caroline Wormell - The University of Sydney, Australia
(Pending)
15:00-15:30 Coffee
15:30-17:00 Unstructured discussions
17:00-18:00 Welcome Reception
Tue 07 Jul 2026
09:00-09:25 Registration and refreshments
09:25-09:30 Housekeeping and Welcome
09:30-10:30 Verified error bounds for sparse systems
Siegfried Rump - Hamburg University of Technology, Germany
The solution of sparse systems is ubiquitous in numerical computations. Despite several efforts, there were no satisfactory method for computing verified bounds for the solution and was one of the “Grand Challenges” in verification methods for decades. In this talk we present two algorithms to compute entrywise error bounds for the solution of general real or complex sparse systems with condition number up to the limit 1016 7 . Our algorithms split into three subalgorithms for symmetric positive definite, symmetric indefinite and general input matrix $A$. A key point is a factorization of $A$ into $L_1L_2$ such that $L_1$ and $L_2$ have identical sets of singular values with the smallest one close to $\sigma_{\mathrm{min}}(A)^{1/2}$. A mathematically correct lower bound on $\sigma_{\mathrm{min}}(L_1) = \sigma_{\mathrm{min}}(L_2)$ is then computed using $L_1^T L_1$. Based on that a second method exploring the inertia of a symmetric/Hermitian matrix is presented. It is often slower but more robust, i.e., it may produce verified inclusions where the first method fails. We show how to compute inclusions with almost maximal accuracy for all entries, i.e., all bounds differ by few bits. That is based on a fast method to compute accurate approximations and bounds for extremely ill-conditioned dot products with a very efficient Matlab implementation. Both approaches are used to compute verified error bounds for the solution of least squares problems and for underdetermined linear systems. Inclusions of the solution of general real or complex systems of nonlinear equations with sparse Jacobi matrix are computed by transforming the problem into a linear system with point matrix and interval right hand side. All algorithms are implemented in pure Matlab/Octave and included from Version 14 of INTLAB, the Matlab/Octave toolbox for verified computations.
10:30-11:00 (TBC)
Nicolae Mihalache - Univ Paris-Est Creteil, France
(Pending)
11:00-11:30 Coffee
11:30-12:15 Rigorous computation of renormalization fixed points using Chebyshev series
Maxime Breden - École Polytechnique, France
(Pending)
12:15-13:00 Computer Assisted Proofs in Julia applied to Area Preserving Twists Maps
George Browne - The Open University, England
(Pending)
13:00-14:00 Lunch
14:00-14:30 Existence of cycles of the doubling operator for coupled maps
Zainab Rahman - University of Portsmouth, England
(Pending)
14:30-15:00 A computer-assisted proof of dynamo growth in the stretch-fold-shear map
Benjamin Mestel - Open University (Retired), England
(Pending - On behalf of Farhana Pramy)
15:00-15:30 Coffee
15:30-17:00 Unstructured discussions
17:00-18:00 Pizza Evening & Networking
Wed 08 Jul 2026
09:00-09:25 Registration and refreshments
09:25-09:30 Housekeeping and Welcome
09:30-10:15 Computer assisted proofs for invariant manifolds and their use in connecting orbit problems
Jason Mireles-James - Florida Atlantic University, USA
Some interesting applications to celestial mechanics and geodesic flow, helped by some advances made over the last few years on validated numerics for the DFT (the same technology that helped us do our Feigenbaum fixed point paper).
10:15-11:00 Arnold Diffusion in the Three-Body Problem
Maciej Capinski - AGH University Kraków, Poland
We present a computer-assisted methodology based on the propagation of topological discs and discuss its applications to Arnold diffusion and blenders in celestial mechanics.
11:00-11:30 Coffee
11:30-12:00 Computer-assisted proof of existence and stability of solitary waves in the Whitham equation
Matthieu Cadiot - École Polytechnique, France
The Whitham equation is a nonlocal model used to study shallow water waves, capturing complex phenomena such as wave breaking, peaking, and various traveling wave solutions. In this talk, I will present a computer-assisted methodology for studying solitary waves—traveling waves that vanish at infinity. In particular, the method provides a framework for the constructive existence proof of a true solution in the close vicinity of an approximate, numerically computed solution. Furthermore, the tight control obtained over the solution enables us to enclose the spectrum of the linearization at the solitary wave, leading to a rigorous and conclusive stability analysis.
12:00-12:30 Computer Assisted Proofs for Nonlinear Problems in the Borel Plane and Validated Numerics for Complex Convolutions
Juan Miranda - Florida Atlantic University, USA
(Pending)
12:30-13:00 (TBC)
Julia Slipantschuk - University of Bayreuth, Germany
(Pending)
13:00-14:00 Lunch
14:00-18:00 HALF DAY SUGGESTIONS:
Wednesday has been planned as a half-day at the ICMS to provide participants with opportunities to network and explore the historic city of Edinburgh together in the afternoon. A number of activities are suggested and some will be led by the organisers.
Tour of the James Clerk Maxwell House, 14 India Street
David Kerridges - James Clerk Maxwell Foundation, Scotland
Tour of Old Town, Royal Mile
Dean Village
Walk to Arthur’s Seat
?
Thu 09 Jul 2026
09:00-09:25 Registration and refreshments
09:25-09:30 Housekeeping and Welcome
09:30-10:30 The CAPD library - a tool for validation in dynamical systems
Daniel Wilczak - Jagiellonian University in Kraków, Poland
The CAPD library [1,2] is a C++ library devoted to validated numerics for dynamical systems. It has been developed for over 30 years by a research team at the Jagiellonian University in Kraków, Poland. The library is mostly oriented towards continuous-time systems and implements rigorous integrators for ODEs, higher order variational equations [3,4], differential inclusions [5], and a class of dissipative PDEs [6]. In the talk I’m going to present the basic interface of the library, then give a few one-screen short yet not very trivial case studies. I will present an application of the library to prove the existence of a uniformly hyperbolic chaotic attractor in a 4D non-autonomous ODE [7]. References: [1] https://github.com/CAPDgroup/CAPD [2] T. Kapela, M. Mrozek, D. Wilczak, P. Zgliczyński. CAPD::DynSys: a flexible C++ toolbox for rigorous numerical analysis of dynamical systems. Commun Nonlinear Sci Numer Simul 2021;101:105578. [3] P. Zgliczyński, $C^1$-Lohner algorithm, Found. Comp. Math, 2(4), pp.429-465 [4] D. Wilczak, P. Zgliczyński, $C^r$-Lohner algorithm, Schedae Informaticae 20, 9-46, 2011. [5] T. Kapela, P. Zgliczyński, A Lohner-type algorithm for control systems and ordinary differential inclusions, Disc. Cont. Dyn. Sys-B, 11(2), pp.365-385 [6] D. Wilczak, P. Zgliczyński. A geometric method for infinite-dimensional chaos: Symbolic dynamics for the Kuramoto-Sivashinsky PDE on the line. J Differential Equations 2020;269(10):8509–48 [7] D. Wilczak, Uniformly hyperbolic attractor of the Smale-Williams type for a Poincaré map in the Kuznetsov system, SIADS. 9 (2010), 1263-1283.
10:30-11:00 Rigorous integration of differential inclusions and delay differential equations in the CAPD library
Tomasz Kapela - Jagiellonian University in Kraków, Poland
(Pending)
11:00-11:30 Coffee
11:30-12:15 Rigorous integration of dissipative PDEs on the torus
Piotr Zgliczynski - Jagiellonian University in Kraków, Poland
We will describe the proof of the existence of symbolic dynamics for the Kuramoto-Sivashinsky PDE on the line: a semiconjugacy with the Bernoulli shift, the existence of countably many periodic orbits and homo- and heteroclinic connections between them. On this example of computer assisted proof we would like to explain how to perform rigorous numerics for dissipative PDEs with periodic boundary conditions and how to use finite dimensional tools from dynamics in the context of dissipative PDEs.
12:15-13:00 Computer-assisted proofs for periodic solutions in state-dependent delay equations
Jean-Philippe Lessard - McGill University, Canada
(Pending)
13:00-14:00 Lunch
14:30-15:00 Taylor models in Julia
Luis Benet Fernández - Universidad Nacional Autónoma de México (UNAM), Mexico
(Pending)
15:00-15:30 Coffee
15:30-17:00 Unstructured discussions
?
Fri 10 Jul 2026
09:00-09:25 Registration and refreshments
09:25-09:30 Housekeeping and Welcome
09:30-10:15 Lower bounds on the Hausdorff dimension of some Julia sets
Igors Gorbovickis - Constructor University, Germany
(Pending)
10:15-11:00 On attractors of Fibonacci maps
Artem Dudko - Institute of Mathematics of the Polish Academy of Sciences (IM PAN), Poland
In 1990s Bruin, Keller, Nowicki, and van Strien showed that smooth unimodal maps with Fibonacci combinatorics and sufficiently high degree of a critical point have a wild attractor, i.e. their metric and topological attractors do not coincide. However, until recently there were no reasonable estimates on the degree of the critical point needed. In the talk I will present a constructive approach for studying attractors of maps, which are periodic points of a renormalization. Using this approach and rigorous computer estimates, we show that the Fibonacci map of degree d=3.8 does not have a wild attractor, but that for degree d=5.1 the wild attractor exists. The talk is based on a joint work with Denis Gaidashev.
11:00-11:30 Coffee
11:30-12:00 (TBC)
Jeremy Parker - University of Dundee, Scotland
(Pending)
12:00-12:30 (TBC)
Olivier Henot - National Taiwan University, Taiwan
(Pending)