This talk is about the formal verification of numerical programs and algorithms. We will go from the motivations and usefulness of a higher guarantee, to the actual verification of C programs, through the formalization in Rocq of both computer arithmetic and applied mathematics. Applications will range from floating-point algorithms and programs from the literature to the work-in-progress formalization of the finite element method.
In this joint work with Carine Pivoteau, we extend the leap generation process to supercritical composition schemes C=A∘B, yielding an exact-size sampler of linear time complexity (under conditions on the sampling complexity in A and B). While exact uniformity of the distribution is lost in general, asymptotic uniformity holds: the total variation distance to the uniform distribution is ∼c/n1/2 for some explicit c, and can be made smaller using a simple rejection step.
A motivation for this work is that these leap generators can be applied to classes of unlabeled rooted trees such as Pólya trees. Experiments confirm the efficiency of the method and closeness to the uniform distribution.
Leap generators can also be developed for certain critical composition schemes, those relating families of planar maps, the total variation distance to the uniform distribution being this time ∼c/n1/3 for some explicit c.
Localisation
Salle de séminaire 4B125 (bâtiment Copernic)
5 Boulevard Descartes 77420 Champs-sur-Marne