Année : 2011

Intervenants : Patrick Cousot, Radu Iosif, Sandrine Blazy, Sébastien Bardin

Dates : 9 – 12 janvier 2012 – ENS Lyon

Programme (prévisionnel)

1- Interprétation abstraite : application à la vérification (P. Cousot)

• Interprétation abstraite
• Estimation de la précision de logiciels numériques
• Vérification de systèmes complexes intégrés sur puce
• Vérifications statiques sur des logiciels critiques embarqués temps-réel
• Vérification de la sécurité de protocoles cryptographiques

2- Model-checking (R. Iosif)

• Classical first- and second-order logic, finite word and tree automata, closure properties and language emptiness.
• Relationship between Weak Monadic Second-Order Logic and finite automata. Infinite automata on words (Buechi, Mueller) and on trees (Rabin) automata, and their relationship with Monadic Second-Order Logic.
• LTL Model Checking and applications

3- Certified compilation (S. Blazy)

• Formally verified compiler
• Software proof codesign
• Translation validation
• Proof carrying code

4- Test (S. Bardin)

• Couverture structurelle et mutations
• Tests de régression
• Exécution dynamique symbolique
• Bounded model-checking

Correspondant local : Ch. Alias
Page web de l’école

 

Justin Romberg
http://users.ece.gatech.edu/justin/Justin_Romberg.html
School of Electrical and Computer Engineering, Georgia Tech

VENUE

ENS Lyon, Site Jacques Monod.
Room: Amphitheater B – 3rd floor

(local correspondant: Paulo Gonçalves)

PROGRAM and MATERIAL

Basis decompositions and frames (3-4 hours)
[notation, basis, frames, dct-notes, wavelets, sparsity-overview]

• fundamentals of basis and frame decompositions
• the discrete cosine transform and applications to image/video compression
• the lapped orthogonal transform
• wavelets
• thresholding for noise reduction

Sparsest decomposition from a dictionary (3-4 hours)
[lecture-2-1-sparseapprox, lecture-2-2-bp, lecture-2-3-upsparse]

• omp and basis pursuit for selecting atoms
• uncertainty principles and sparsest decomposition
• the « spikes+sines » dictionary
• general unions of orthobases

Introduction to compressive sampling and applications (2 hours)
[csoverview-part1,csoverview-part2,csoverview-part3,csoverview-part4] 

Recovering sparse vectors from linear measurements (6 hours/ 1 day)
[lecture-3-1-invprobs,lecture-3-2-ls,lecture-3-3-l1dual,lecture-3-4-l1cone,lecture-3-5-stable]

• review of classical least-squares theory:
• the svd, pseudo-inverse, stability analysis, regularization
• sparse recovery conditions: l1 duality
• sparsest decomposition revisited (with random support)
• the restricted isometry property and sparse recovery
• l1 for perfect recovery from noise-free measurements
• l1 stability
• l2 stability

Random matrices are restricted isometries (2 hours)
[lecture-4-1-gaussrip] 

Optimization (6 hours / 1 day)
[lecture-5-1-sdcg,lecture-5-2-newtonlog,lecture-5-3-streamingl2,lecture-5-4-streamingl1,lasso-dual-notes]
[siamOptimTalk] 

• conjugate gradients
• newton iterations
• newton iterations
• log-barrier methods
• first-order l1 solvers
• greedy algorithms and iterative thresholding
• recursive least-squares
• the Kalman filter
• dynamic l1 updating

Low-rank recovery (2 hours)

TIMETABLE

Monday 9:  10:00am – 12:00am ; 2:00pm – 5:00pm  (5 hours)
Tuesday 10:  9:30am – 12:00am ;  2:00pm – 5:00pm  (5,5 hours)
Wednesday 11:  9:30am – 12:00am ; 2:00pm – 5:00pm  (5,5 hours)
Thursday 12:  9:30am – 12:30pm ; free afternoon  (3 hours)
Friday 13:  9:00am – 12:00am ; 2:00pm – 4:00pm  (5 hours)

Intervenants : Laurent Bienvenu, Alexander Shen

En cette année 2012, qui célèbre les 100 ans après la naissance d’Alan Turing, nous présenterons les bases de la théorie qu’il a contribué à fonder, celle de la calculabilité. Nous rappellerons les concepts de base (machines de Turing, fonctions calculables) pour arriver rapidement à présenter quelques résultats et techniques fondamentaux de la calculabilité.

Le programme (prévisionnel) du cours est le suivant.

1. Rappels de concepts de base
   • Machines de Turing
   • Ensembles et fonctions calculables, ensembles récursivement énumérables
2. Indécidabilité
   • Problème de l’arrêt. Indécidabilité, et many-one complétude
   • Autres exemples de problèmes indécidables équivalents à l’arrêt:
     équations diophantiennes, problème du mot dans les semi-groupes,
     logique du premier ordre, etc.
3. Oracles et réductions
   • Machines de Turing à oracle
   • Réduction Turing, degrés de Turing
4. Hiérarchie arithmétique
   • Le jump comme opérateur sur les degrés.
   • Lemme de Schoenfield
   • La hiérarchie arithmétique et ses liens avec l’opérateur de jump
   • Complétude des ensembles \Sigma^0_n et \Pi^0_n, exemples de problèmes complets
5. Résultats avancés sur les degrés
   • Existence de degrés non comparables (2 preuves: par diagonalisation et probabiliste par le théorème de Sacks)
   • Existence de deux degrés r.e. par la méthode de priorité de Friedberg-Muchnik
   • Existence d’un degré de Turing minimal
   • (Plus si le temps le permet: degrés « low », « high » et leur existence)
6. Calculabilité sur les réels
   • Définition des fonctions calculables sur les réels et leurs propriétés élémentaires
   • Analyse calculable: théorèmes effectifs et non-effectifs

Les exposés seront donnés en anglais.

Dates : 16 au 20/01/2011

Planning:

– Lundi: 10h30-12h cours/TD; 14h-16h30 cours/TD
– Mardi: 10h-12h cours ; 14h-15h30 cours; 16h-17h30 TD
– Mercredi: 10h-12h cours ; 14h-15h30 cours; 16h-17h30 TD
– Jeudi: 10h-12h cours ; 14h-15h30 cours; 16h-17h30 TD
– Vendredi: 10h-12h cours ; 14h-15h30 cours; 16h-17h30 TD

Examen vendredi jusqu’à 18h3o (à confirmer)

Correspondante locale : Natacha Portier

Intervenants : Frédéric Giroire, Frédéric Havet et Nicolas Nisse

Dates : du 23 au 27 janvier 2012, à ENS Lyon, amphi B (sauf la séance de TP en E001)

Programme

Lundi
9h00 – 11h30
13h30 – 15h00
15h30 – 17h30
Introduction, Modelisation de problemes en PL, Simplexe approche geometrique.

Mardi
9h00 – 11h30 Dualité I
14h00 – 15h30 Dualité II
16h00 – 17h30 Ellipsoïde.

Mercredi
9h00 – 11h30 TP
13h30 – 15h00 Relaxation fractionnaire: Totale unimodularite.
15h30 – 17h30 Relaxation Lagrangienne.

Jeudi
9h – 11h30 Relaxation fractionnaire: Arrondis deterministes et aleatoires, integral gap.

Vendredi
9h – 11h30 Algorithmes primal-dual.
13h30 – 15h00 Examen.

Correspondant local : Nicolas Trotignon

Magnifiques notes de cours :
Introduction to linear programming duality
Ellipsoid method
Fractional relaxation
Lagrangian relaxation

Intervenants : Maria Potop-Butucaru, Sébastien Tixeuil

Dates : 6 au 10 février 2012

Résumé de l’école de recherche :

L’algorithmique distribuée est l’algorithmique des réseaux et des systèmes distribués. Dans un algorithme distribué, les machines qui participent au calcul collaborent à une tâche commune malgré des informations qui ne peuvent s’échanger que localement, malgré des vitesses de calcul et de communication qui diffèrent parfois significativement, malgré des connaissances sur le système global qui ne sont que parcellaires, malgré des pannes de certaines de ces machines qui surviennent inopinément, malgré des attaques sur des machines critiques qui surviennent au pire moment, malgré des machines qui vont et qui viennent au gré de la volonté de leurs utilisateurs. En  somme, il s’agit pour ces machines de collaborer malgré l’adversité.

L’objectif du cours est de proposer un panorama des recherches récentes en algorithmique distribuée, tant du point de vue de la tolérance aux fautes et aux attaques (auto-stabilisation, comportements Byzantins, etc.), que de celui de la coordination distribuée (cohortes de robots, agents mobiles, etc.).

Voir la page de l’école de recherche.

Correspondant local : Eddy Caron

Intervenants : Sylvain Lefebvre (INRIA Nancy-Grand Est), Bruno Lévy (INRIA Nancy Grand-Est).

Thème :Ce cours introduit les algorithmes fondamentaux utilisés en synthèse d’images, avec un accent en particulier sur le calcul rapide pour l’affichage temps réel (simulateurs, pré-visualisation, jeux). Les techniques de lancer de rayon et rendu projectif seront abordées, avec quelques excursions vers des domaines actifs de recherche comme la modélisation géométrique, le placage de texture et la génération procédurale de contenu. Le cours comprend également une introduction à la programmation des cartes graphiques parallèles via OpenGL et OpenCL.

Date : 13/02-17/02/2012

Emploi du temps :

Lundi 13/02 : 14h-17h30 cours

Mardi 14/02 9h-12h30 cours, 14h-16h cours

Mercredi 15/02 14h-17h30 cours

Jeudi 16/02 9h-13h TD

Vendredi 9h-12h30 cours, 14h-18h TD

Correspondant local : Guillaume Hanrot