Current

Unless stated otherwise, the seminar takes place on Tuesdays, from 10 to 11, in room 385 at IMB. To get announcements, you can subscribe to the mailing-list.

2019-11-19
10:00
Salle 2
Maria Dostret (EPFL)
Exact Semidefinite Programming Bounds for Packing Problems
Semidefinite Programming (SDP) is a powerful tool to obtain upper bounds for packing problems. For example, one can consider the kissing problem of the hemisphere in dimension 8 which asks for the maximal number of pairwise non-overlapping spheres which can simultaneously touch a central hemisphere in 8-dimensional Euclidean space. The E8 lattice gives a kissing configuration of 183 points. Moreover, using an SDP given by Bachoc and Vallentin one gets an upper bound of 182.99999999996523. Hence, the optimal value is 183. But how can we obtain the exact rational solution of the SDP based on the floating point results given by the SDP solver?
In this talk, I will explain how we can determine the exact result of the SDP. Furthermore, we use these techniques to obtain exact results for the kissing problem of the hemisphere in dimension 8 as well as for other packing problems.

Using the exact rational solution for the kissing problem of the hemisphere, we can prove that the optimal kissing configuration is unique up to isometry.

This is a joint work with David de Laat and Philippe Moustrou.
2019-11-26
10:00
Salle 2
Alice Pellet-Mary (ÉNS de Lyon)
An LLL Algorithm for Module Lattices
A lattice is a discrete subgroup (i.e., $\mathbb Z$-module) of $\mathbb R^n$ (where $\mathbb Z$ and $\mathbb R$ are the sets of integers and real numbers). The LLL algorithm is a central algorithm to manipulate lattice bases. It takes as input a basis of a Euclidean lattice, and, within a polynomial number of operations, it outputs another basis of the same lattice but consisting of rather short vectors.
On the cryptographic side, many algorithms based on lattices in fact use structured lattices, in order to improve the efficiency of the schemes. Most of the time, these structured lattices are $R$-modules of small dimension, where $R$ is the ring a integers of some number field. It is then tempting to try and adapt the LLL algorithm, which works over lattices (i.e., $\mathbb Z$-modules), to these $R$-modules.

All the previous works trying to solve this question focused on rings of integers $R$ that were Euclidean, as the LLL algorithm over $\mathbb Z$ crucially rely on the Euclidean division. In this talk, I will describe the first LLL algorithm which works in any ring of integers $R$. This algorithm is heuristic and runs in quantum polynomial time if given access to an oracle solving the closest vector problem in a fixed lattice, depending only on the ring of integers R.

This is a joint work with Changmin Lee, Damien Stehlé and Alexandre Wallet
2019-12-02
TBD
TBD
Tony Ezome (Université des Sciences et Techniques de Masuku (USTM), Franceville, Gabon)
TBA
2019-12-17
10:00
Salle 2
Raphael Rieu-Helft (Université Paris-Sud)
How to Get an Efficient yet Verified Arbitrary-Precision Integer Library
We present a fully verified arbitrary-precision integer arithmetic library designed using the Why3 program verifier. It is intended as a verified replacement for the mpn layer of the state-of-the-art GNU Multi-Precision library (GMP).
The formal verification is done using a mix of automated provers and user-provided proof annotations. We have verified the GMP algorithms for addition, subtraction, multiplication (schoolbook and Toom-2/2.5), schoolbook division, divide-and-conquer square root and modular exponentiation. The rest of the mpn API is work in progress. The main challenge is to preserve and verify all the GMP algorithmic tricks in order to get good performance.

Our algorithms are implemented as WhyML functions. We use a dedicated memory model to write them in an imperative style very close to the C language. Such functions can then be extracted straightforwardly to efficient C code. For medium-sized integers (less than 1000 bits, or 100,000 for multiplication), the resulting library is performance-competitive with the generic, pure-C configuration of GMP.