Attention: programme préliminaire susceptible d'être modifié.
| 16:00-17:00 | Accueil | |
| 17:00-18:00 | MirageOS ou la quête d'un OS plus petit et plus sûr | Thomas Gazagnaire |
| 18:00-18:30 | Domaines spatio-temporels: un tour d'horizon | David Janin |
| 18:30-19:00 | HOcore en HOcore | Lionel Zoubritzky et Alan Schmitt |
| 19:00 | Dîner |
| 9:00-10:30 | La programmation de micro-contrôleurs dans des langages de haut niveau (partie I) | Steven Varoumas, Benoit Vaugon et Emmanuel Chailloux |
| 10:30-11:00 | Pause | |
| 11:00-11:30 | Vérification de programmes OCaml fortement impératifs avec Why3 | Jean-Christophe Filliatre, Mário Pereira et Simão Melo de Sousa |
| 11:30-12:00 | A Value analysis based memory model | Quentin Bouillaguet, François Bobot, Boris Yakobowski et Mihaela Sighireanu |
| 12:00-12:20 | Un mécanisme d'extraction vers C pour Why3 | Raphaël Rieu-Helft |
| 12:20-14:00 | Déjeuner | |
| 14:00-15:30 | Activités libres | |
| 15:30-17:00 | La programmation de micro-contrôleurs dans des langages de haut niveau (partie II) | Steven Varoumas, Benoit Vaugon et Emmanuel Chailloux |
| 17:00-17:30 | Pause | |
| 17:30-18:00 | Towards Secure and Trusted-by-Design Smart Contracts | Zaynah Dargaye, Onder Gurcan, Florent Kirchner et Sara Tucci |
| 18:00-18:30 | Liquidity : OCaml pour la Blockchain | Çağdaş Bozman, Mohamed Iguernlala, Michael Laporte, Fabrice Le Fessant et Alain Mebsout |
| 18:30-19:00 | agdarsec - Total Parser Combinators | Guillaume Allais |
| 19:00 | Dîner |
| 9:00-10:30 | Interactive Verification of Imperative Programs using CFML (partie I) | Arthur Charguéraud |
| 10:30-11:00 | Pause | |
| 11:00-11:30 | Hydra Ludica: Une preuve d'impossibilité de prouver simplement | Pierre Castéran |
| 11:30-11:50 | OCaml étendu avec du filtrage par comotifs | Paul Laforgue et Yann Régis-Gianas |
| 11:50-12:10 | Définir le fini : deux formalisations d'espaces de dimension finie | Florian Faissole |
| 12:10-14:00 | Déjeuner | |
| 14:00-15:30 | Activités libres | |
| 15:30-17:00 | Interactive Verification of Imperative Programs using CFML (partie II) | Arthur Charguéraud |
| 17:00-17:30 | Pause | |
| 17:30-18:00 | Preuves constructives de programmes probabilistes | Florian Faissole et Bas Spitters |
| 18:00-18:20 | Génération aléatoire de programmes guidée par la vivacité | Gergö Barany et Gabriel Scherer |
| 18:20-18:40 | Why3 a dit : gardez le contrôle en toute situation | Jean-Christophe Léchenet, Nikolai Kosmatov et Pascale Le Gall |
| 18:40-19:00 | Vérification automatique de chaînes de fonctions de sécurité dans des réseaux programmables SDN avec Synaptic | Nicolas Schnepf, Rémi Badonnel, Abdelkader Lahmadi et Stephan Merz |
| 19:00 | Dîner |
| 9:00-10:00 | Garantir l'intégrité et la provenance des données par typage, et application à la démonstration automatique modulaire et sans bugs | Stéphane Graham-Lengrand |
| 10:00-10:30 | Pause | |
| 10:30-10:50 | Simplification efficace pour la théorie des tableaux | Benjamin Farinier, Sébastien Bardin et Robin David |
| 10:50-11:10 | Programmer des Chatbots en OCaml avec Watson Conversation Service | Guillaume Baudart, Louis Mandel et Jerome Simeon |
| 11:30 | Repas à emporter |