Lundi 28 mai #

9h30-10h00 Café

10h00-13h00 Vérification déductive autour de l'outil Why3 (Andrei Paskevich)

  • 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)

  • 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)

  • 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)

  • 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)

  • 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é

Add new attachment

Only authorized users are allowed to upload new attachments.
« This page (revision-23) was last changed on 22-mai-2018 20:15 by Radu Iosif