Lundi 28 mai
9h30-10h00 Café
10h00-13h00 Vérification déductive autour de l’outil Why3 ([Andrei Paskevich|http://tertium.org/])
- 10h00-10h50 Raphaël Rieu-Helft »How to Get an Efficient yet Verified Arbitrary-Precision Integer Library »
- 11h00-11h50 Mohamed Iguernelala »Alt-Ergo : un solveur SMT pour la preuve de programmes »
- 12h00-12h50 Claire Dross »Why3 as Intermediate Language for SPARK »
13h00-14h00 Dejeuner
14h00-17h00 Exposés courts
- 14h00-14h30 Vincent Penelle »Rewriting Higher-order Stack Trees »
- 14h30-15h00 Filip Mazowiecki »When is Containment Decidable for Probabilistic Automata? »
15h00-15h30 Pause café
- 15h30-16h00 Bruno Guillon »Undecidability of MSO+ultimately periodic »
- 16h00-16h30 Nathan Lhote »A logic for transductions with regular synthesis »
Mardi 29 mai
9h30-10h00 Café
10h00-13h00 Vérification et synthèse multi-critères ([Mickael Randour|http://math.umons.ac.be/staff/Randour.Mickael/])
- 10h00-10h50 Sebastian Junges »Parameter Synthesis for Markov Chains »
- 11h00-11h50 Laure Daviaud »A pseudo-quasi polynomial algorithm for mean-payoff parity games »
- 12h00-12h50 Mickael Randour »Rich behavioral models: illustration on journey planning »
13h00-14h00 Dejeuner
14h00-16h00 Apprentissage et vérification I ([Nathanaël Fijalkow|https://nathanael-fijalkow.github.io/])
- 14h00-14h50 Nathanaël Fijalkow »Verifying learning algorithms: state of the art »
- 15h00-15h50 Oded Maler »Automaton learning over large alphabets »
16h00-16h30 Pause café
16h30-17h30 Exposés courts
- 16h30-17h00 Aline Goeminne »Constraint Problem for Weak Subgame Perfect Equilibria with omega-regular Boolean Objectives »
- 17h00-17h30 Marion Hallet »Dynamics on sequential games and games played on graph »
Mercredi 30 mai
9h00-12h00 Vérification de programmes : mémoire et concurrence ([Étienne Lozes|http://www.i3s.unice.fr/~elozes/])
- 9h00-9h50 Nicolas Peltier »On the Expressive Completeness of Bernays-Schönfinkel-Ramsey Separation Logic »
- 10h00-10h50 Jacques-Henri Jourdan »RustBelt et Iris – Sûreté du système de types de Rust et logique de séparation concurrente extensible d’ordre supérieur »
- 11h00-11h50 Mihaela Sighireanu »Separation Logic for Static Analysis of Dynamic Memory Allocators »
12h00-13h00 Apprentissage et vérification II ([Nathanaël Fijalkow|https://nathanael-fijalkow.github.io/])
- Rémi Eyraud »Spectral Learning of Weighted Automata: from theory to a toolbox »
13h00-14h00 Dejeuner
14h00-15h00 Exposés courts
- 14h00-14h30 Alessio Mansutti »The Effects of Adding Reachability Predicates in Propositional Separation Logic »
- 14h30-15h00 Cristina Serban »Complete Cyclic Proof Systems for Inductive Entailments »
- 15h00-15h30 Raphaël Cauderlier »Vérification du conteneur de liste bornée »
15h30-16h00 Pause café