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-12-10
10:00
Salle 2
Développeurs LFANT (IMB)
Hacking session
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.
2020-01-07
10:00
Salle 385
Jean-Marc Couveignes (IMB)
Compter les corps de nombres
2020-01-14
10:00
Salle 385
Abdoulaye Maiga (IMB)
TBA
2020-02-04
10:00
Salle 385
Aude Le Gluher (LORIA)
TBA
2020-02-18
10:00
Salle 385
Alex Bartel (University of Glasgow)
TBA