Lieu: LMF, bâtiment 650, salle des thèses (435)
Attention, accès difficile pour cause de chantier en cours
- Porte principale batiment 650 condamnée
- Point de rendez-vous pour les visiteurs sans badge : sortie de secours sud-est, marqueur bleu sur ce plan
- Pour vous faire entrer, appelez Claude au 06 51 53 21 98
Participation possible en visio sur BBB Inria/ProofInUse
Programme
Les slides sont accessibles en cliquant sur les titres d'exposés.- 09h30: Welcome coffee, pour celles et ceux qui sont sur place, en salle café LMF, bloc sud-est, 1er étage au fond du couloir.
- 10h00: Validation de contre-exemples avec Why3 et
Spark Solène Moreau et Claude Marché
Bonus: un lien pour celles et ceux qui n'auraient pas la ref et aussi des infos sur Lunar IceCube
- 10h45: Vers un écosystème de packages pour Why3 Loïc Correnson
- 11h15: pause
- 11h30: Preuve de programmes Rust avec Creusot, cas des itérateurs Xavier Denis
- 12h30: Pause déjeuner
- 14h00: Preuves de code C bas-niveau avec J3 Guillaume Cluzel et Raphaël Rieu-Helft
- 14h45: Étude de cas d'un code C numérique : Log-Sum-Exp Paul Bonnot
- 15h30: pause
- 16h00: Alt-Ergo 2.5: vers un solveur modèle Pierre Villemot et/ou Guillaume Bury
- 16h30: discussions diverses
- Claire Dross, retour sur un séminaire Dagsthul récent
- Prochaine journée
- ...
- 17h00: End of meeting
Participants
Sur place:- Andrei Paskevich, LMF/Toccata
- Armaël Guéneau, LMF/Toccata
- Benjamin Monate, TrustInSoft
- Chareton Christophe, CEA
- Christine Paulin, LMF
- Claude Marché, LMF/Toccata
- Florian Faissole, MERCE (l'après-midi)
- François Bobot, CEA
- Guillaume Bury, OCamlPro
- Guillaume Cluzel, TrustInSoft
- Jacques-Henri Jourdan, LMF
- Jean-Christophe Filliâtre, LMF/Toccata
- Josué Moreau, LMF/Toccata
- Jérôme Ricciardi, CEA/LMF
- Loïc Correnson, CEA
- Mihaela Sighireanu, LMF
- Milan Martos, OCamlPro
- Muriel Shan Sei Fan, OCamlPro
- Paul Bonnot, LMF/Toccata
- Paul Géneau de Lamarlière, LMF/Toccata
- Pierre Villemot, OCamlPro
- Raphaël Rieu-Helft, TrustInSoft
- Solène Moreau, LMF/Toccata
- Steven De Oliviera, OCamlPro
- Sylvie Boldo, LMF/Toccata
- Xavier Denis, LMF/Toccata
- Yannick Moy, AdaCore
- Allan Blanchard, CEA
- Claire Dross, AdaCore
- David Mentré, MERCE
- Denis Cousineau, MERCE
- Fabrice Le Fessant, OCamlPro
- Virgile Prevosto, CEA