Category: Archives

Dates: December 9-13, 2013.

School outline and timetable .

Local contact :Natacha Portier.

Registration

Registration is free, but the number of participants is limited. Registration includes neither housing nor meals (though for lunch the attendees will be granted access to the student cafeteria). Registration should be made before November 29, 2013 by clicking on this link, filling the form and sending the e-mail message. You will receive a confirmation as soon as possible.

Alternatively, you can copy/paste and fill the form below, then send it by e-mail to nicole.meftah@ens-lyon.fr with the subject line “Registration form — research school 1”

First Name:
Last Name:
Institution:
Position (MSc student, PhD student, researcher, etc.):
E-mail address:
wishes to attend the research school “Algorithmic Game Theory”, taking place at ENS Lyon, from Dec. 9 to Dec. 13, 2013.

Dates: January 13-17, 2014.

Web site.

Local contact : Laure Gonnord.

Registration

Registration is free, but the number of participants is limited. Registration includes neither housing nor meals (though for lunch the attendees will be granted access to the student cafeteria). Registration should be made before January 3, 2014 by clicking on this link, filling the form and sending the e-mail message. You will receive a confirmation as soon as possible.

Alternatively, you can copy/paste and fill the form below, then send it by e-mail to nicole.meftah@ens-lyon.fr with the subject line “Registration form — research school 2”

First Name:
Last Name:
Institution:
Position (MSc student, PhD student, researcher, etc.):
E-mail address:
wishes to attend the research school “Synchronous Approaches for Embedded Systems”, taking place at ENS Lyon, from Jan. 13 to Jan. 17, 2014.

Speakers: André Platzer and Sarah Loos.

Dates: January 20-24, 2014.

Web page.

Local contact: Filippo Bonchi

Registration

Registration is free, but the number of participants is limited. Registration includes neither housing nor meals (though for lunch the attendees will be granted access to the student cafeteria). Registration should be made before January 10, 2014 by clicking on this link, filling the form and sending the e-mail message. You will receive a confirmation as soon as possible.

Alternatively, you can copy/paste and fill the form below, then send it by e-mail to nicole.meftah@ens-lyon.fr with the subject line “Registration form — research school 3”

First Name:
Last Name:
Institution:
Position (MSc student, PhD student, researcher, etc.):
E-mail address:
wishes to attend the research school “Logic for Dynamical Systems”, taking place at ENS Lyon, from Jan. 20 to Jan. 24, 2014.

January 21-25, 2013, ENS Lyon.

Speakers: Manuel Bodirsky, Michael Pinsker.

A Constraint Satisfaction Problem (CSP) is a computational problem where the task is to decide for a given finite set of variables and constraints whether there is an assignment to the variables that satisfies all constraints. Many computational problems in various areas of theoretical computer science can be modeled in this way.

If the variables take their values in some finite domain, there is a rich universal-algebraic theory that describes those constraint languages whose CSP is NP-hard, and those whose CSP is in P. In this course, we present a powerful generalization of this approach to CSPs where the underlying domain is infinite.
After introducing the necessary background in model theory, the course will also cover recent applications of structural Ramsey theory that have led to complexity classification results for large classes of CSPs.

Outline of the course

Monday: Examples of CSPs from Artificial Intelligence. Primitive positive formulas and NP-hardness proofs. Some efficient algorithms. The Feder-Vardi conjecture.

Tuesday: The universal-algebraic approach. The Inv-Pol Galois correspondence. The core of a structure. The tractability conjecture. Cyclic operations. Exercices.

Wednesday: CSPs on infinite domains. Fraïssé limits, the Ryll-Nardzewski theorem. The Inv-Pol correspondence on infinite domains. The topology of simple convergence.  Henson digraphs and other examples.

Thirsday: Introduction to Ramsey theory. Canonical functions. The classification of Graph-SAT problems.

Friday: Open problems, proposals of research projects. Exam and discussion.

Local contact: Pascal Koiran

Registration

Registration is free, but there is a limit on the number of participants and it does include neither housing nor meals (though for lunch the attendees will be granted access to the student cafeteria). Registration should be made before Monday, December 3, by clicking on this link and filling in and sending the e-mail form. You shall receive a confirmation as soon as possible.

Alternatively, you can copy/paste and fill the following form and send it by e-mail to research.school.1@gmail.com, with subject “Registration form — research school 3”

First Name:
Last Name:
Institution:
Position (MSc student, PhD student, researcher, etc.):
E-mail address:
wishes to attend the research school ‘Constraint satisfaction problems’, taking place at ENS Lyon, from Jan. 21 to Jan. 25.

January 14-18, 2013, ENS Lyon.

Speakers

Francesco Zappa Nardelli (INRIA), Mark Batty (University of Cambridge), Alastair Donaldson(Imperial College London), and Martin Vechev (ETH Zurich)

Slides

Available from here

Abstract

Optimisations performed by the hardware or by high-level language compilers can reorder memory accesses in various subtle ways. These reorderings can sometimes be observed by concurrent programs, exacerbating the usual problems of concurrent programming. The situation is even worse when we abandon traditional shared memory concurrency in favor of graphics processing units (GPUs) or exotic hardware. In these lectures we will cover recent progress in understanding and specifying the behaviour of some major processor architectures and the impact of optimisations performed by high-level programming language compilers, stablishing a solid basis for shared memory programming. We will then explore techniques which can help programmers develop reliable concurrent software by automatically discovering the necessary synchronization. We will also discuss techniques for verification of multicore software, including GPU kernels.

Schedule:

• Monday:
  • 10h30-12h30: Welcome + introduction
  • 14h: Batty: x86TSO
  • 15h30-16h30: TD: x86TSO
• Tuesday
  • 9h-10h30: Batty + Zappa: ARM & Power
  • 11h-12h30: Zappa : Compiler Optimisations + DRF
  • 14h-15h: TD: ARM & Power
  • 15h30-16h30: TD: Compiler Optimisations + DRF
• Wednesday
  • 9h-10h30: Batty : C11
  • 11h-12h30: Vechev (1)
  • 14h-15h: TD : C11
  • 15h30-16h30: TD : Vechev
• Thursday
  • 9h-10h30: Vechev (2)
  • 11h-12h30: Alastair (1)
• Friday
  • 9h-10h30: Alastair (2)
  • 11h-12h30: TD: Alastair
  • 14h-15h30: Mini-exam

For the practical sessions

Please bring your laptop with you. In case you do not have one, please get in contact with Filippo Bonchi (ens-lyon.fr).

Contact: Filippo Bonchi.

Registration

Registration is free, but there is a limit on the number of participants and it does include neither housing nor meals (though for lunch the attendees will be granted access to the student cafeteria). Registration should be made before Monday, January 8, by clicking on this link and filling in and sending the e-mail form. You shall receive a confirmation as soon as possible.

Alternatively, you can copy/paste and fill the following form and send it by e-mail to research.school.1@gmail.com, with subject “Registration form — research school 2”

First Name:

Last Name:

Institution:

Position (MSc student, PhD student, researcher, etc.):

E-mail address:

wishes to attend the research school ‘Semantics and tools for low-level concurrent programming’, taking place at ENS Lyon, from Jan. 14 to Jan. 18.

George Bosilca et Thomas Hérault,

University of Tennessee Knoxville

December 10-14, 2012, ENS Lyon.

During this course, we will discuss fault tolerance techniques for high performance computing systems.

Motivation.

In June 2008, the LANL’s Road Runner computing system was the first to  cross the hallmark of one Petaflop based on the Linpack benchmark (reaching $1.026 \cdot 10^{15}$ double precision floating point operation per second). Today, only 4 years later, the fastest computing system, the Sequoia BlueGene/Q at LLNL, sustains 16.324 Petaflops. Continuing on the same path, it is expected that as early as 2022, computing systems will conquer the 1 Exaflop milestone ($10^18$ flops). After the multicore revolution of 2000, such performance became achievable only by multiplying the number of computing components (cores) in the parallel machine. When the 2008 Road Runner machine had 122,400 cores, distributed over 20,000 heterogeneous nodes, today’s Sequoia systems exhibits no less than 1,572,864 cores, distributed over 100,000 nodes. The drawback of such exponential increase in the number of components is a disruptive decrease in the reliability of the entire

system. Indeed, the Mean Time To Interruption, defined as the average duration for which all the components of the platform behave as specified, is inversely proportional to the number of components in this platform. When in 2009, the MTTI of the largest supercomputers was estimated close to 4 days, it sharply decrease below a single day (19h04 min) in 2011, and projected to continue its descent in the following years (less than 4h by 2015, less than 2h by 2018). While technical breakthrough will hopefully allow the MTTI to remain in a tolerable area, long running applications need an execution environment more flexible, an environment allowing them to survive for longer period of time either algorithmically or by taking advantage of specialized capabilities of the programming model. Unfortunately, current programming paradigms do not account for such a hardware instability; the failure of a single component (be it memory or computing unit, hard

drive or network card) has a drastic and lasting effect on the computation. Even without accounting for the implicit energy costs, in front of the evolving expectations for the next generation computing platforms MTTI, such approaches cannot reasonably lead to sustainable software solutions.

Overview.

This course will highlight the existing solutions, and present parallel algorithms designed to provide correct solutions despite the presence of failures. We will show how the programming environment can be modified to increase the system reliability and sustainability. The course will start with an introduction to High Performance Programming, its challenges and typical algorithms.

Then we present theoretical as well as practical studies of the many fault-tolerant approaches that have been proposed over the years.

Prerequisite.

The course assumes a general knowledge of algorithms and operating system, as well as a basic understanding of machine architecture and network systems.

Update: bring your laptop! Some exercises on machine will be proposed along the course. Attendants are expected to bring a laptop with a possibility to establish a connection to a distant machine (typically, ssh): please write to the local contact (Yves Robert) if this is not possible for you — we should be able to lend a few laptops to participants.

Local contact: Yves Robert.

Registration

Registration is free, but there is a limit on the number of participants and it does include neither housing nor meals (though for lunch the attendees will be granted access to the student cafeteria). Registration should be made before Monday, December 3, by clicking on this link and filling in and sending the e-mail form. You shall receive a confirmation as soon as possible.

Alternatively, you can copy/paste and fill the following form and send it by e-mail to research.school.1@gmail.com, with subject “Registration form — research school 1”

 

First Name:

Last Name:

Institution:

Position (MSc student, PhD student, researcher, etc.):

E-mail address:

wishes to attend the research school ‘Fault tolerance for high performance computing’, taking place at ENS Lyon, from Dec. 10 to Dec. 14

 

Lecturer : Justin Romberg (Georgia Institute of Technology, Atlanta)

Outline of the school :
“The dogma of signal processing maintains that a signal must be sampled at a rate at least twice its highest frequency in order to be represented without error. However, in practice, we often compress the data soon after sensing, trading off signal representation complexity (bits) for some error (consider JPEG image compression in digital cameras, for example). Clearly, this is wasteful of valuable sensing resources. Over the past few years, a new theory of “compressive sensing” has begun to emerge, in which the signal is sampled (and simultaneously compressed) at a greatly reduced rate.
Compressive sensing is also referred to in the literature by the terms: compressed sensing, compressive sampling, and sketching/heavy-hitters.” [by courtesy of: http://dsp.rice.edu/cs]

• Basis decompositions and frames (3-4 hours)
  •  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)
  •    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)
• Recovering sparse vectors from linear measurements (6 hours/ 1 day)
  •    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)
• Optimization (6 hours / 1 day)
  • conjugate gradients
  •   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)

Dates : 9-13/01/2012

Correspondant local : Paulo Goncalves

 

 

Intervenant : François Baccelli (http://www.di.ens.fr/~baccelli/)

The lecture will be taught in English.

Dates : 10 – 14 janvier 2011 – ENS Lyon

Planning:

lundi : 10h30 : 12h30 – 14h00 : 17h00
mardi : 10h00 : 12h00 – 14h00 : 17h00
mercredi : 10h00 : 12h00 – 14h00 : 17h00
jeudi : 10h00 : 12h00 – 14h00 : 17h00
vendredi : 10h00 : 12h00 – 14h00 : 16h00

Objectif: Introduction à la géométrie stochastique et application à la modélisation des communications dans les réseaux sans fil.

Programme (prévisionnel)

Part I – Classical Stochastic Geometry

1. Poisson Point Process
2. Marked Point Processes and Shot-Noise Fields
3. Boolean Model
4. Voronoi Tessellation

Part II – Signal-to-Interference Ratio Stochastic Geometry

5. Signal-to-Interference Ratio Cells
6. Interacting Signal-to-Interference Ratio Cells
7. Signal-to-Interference Ratio Coverage
8. Signal-to-Interference Ratio Connectivity

Part III – Medium Access Control

9. Spatial Aloha: the Bipole Model
10. Receiver Selection in Spatial Aloha
11. Carrier Sense Multiple Access
12. Code Division Multiple Access in Cellular Networks

Part IV – Multihop Routing in Mobile ad Hoc Networks

13. Optimal Routing
14. Greedy Routing
15. Time-Space Routing

Prérequis : Probabilités (à cet effet, les étudiants de M1 sont vivement invités à suivre le cours de L3 “Probabilités – Statistiques“)

Documents de support : monographie “Stochastic Geometry and Wireless Networks” (2009), by F. Baccelli and B. Blaszczyszyn (available on-line at http://www.di.ens.fr/~baccelli/)

Correspondant local : P. Gonçalves.
Sponsor : Pôle ResCom du GDR CNRS ASR

From the 24th to the 28th of January 2011 — ENS Lyon

The lectures will be delivered in English.

Goals

Some of the notable recent successes in automated visual recognition are results of combining advanced visual representations together with powerful machine learning techniques. The objective of this winter school is to provide an overview of basic tools and some latest advances in visual recognition together with the related machine learning algorithms. A particular emphasis will be given on topics related to recognition of objects and human actions in video and still images. Lectures will be given by experts in visual recognition and machine learning. Lectures will be complemented by practical sessions, where participants will obtain hands-on experience with the discussed material.

Speakers :

1. Zaid Harchaoui (INRIA, LEAR, INRIA Rhône-Alpes)
2. Ivan Laptev (INRIA, WILLOW, INRIA Rocquencourt)
3. Cordelia Schmid (INRIA, LEAR, INRIA Rhône-Alpes)
4. Josef Sivic (INRIA, WILLOW, INRIA Rocquencourt)

Tentative outline and schedule of the course

[L] means a lecture, and [E] means an exercise session.

If possible, please bring a laptop with you for the exercise sessions.

• Monday, January 24
  • [L] 8:15 AM – 9:15 AM. Unsupervised learning (Zaid Harchaoui). Slides available here, here and here.
• [L] 9:30 AM – 10:30 AM. Unsupervised learning (Zaid Harchaoui)
• [E] 10:45 AM – 11:45 AM. Unsupervised learning (Zaid Harchaoui)
• [L] 1:30 PM – 2:30 PM. Image features (Cordelia Schmid). Slides available here and here (ppt files) or here and here (pdf files).
• [L] 2:45 PM – 3:45 PM. Image features (Cordelia Schmid)
• [E] 4:00 PM – 5:00 PM. Image features (Cordelia Schmid, Josef Sivic)
• Tuesday, January 25
  • [L] 8:15 AM – 9:15 AM. Camera geometry and Image Alignment (Josef Sivic). Slides available here.
  • [L] 9:30 AM – 10:30 AM. Camera geometry and Image Alignment (Josef Sivic)
  • [E] 10:45 AM – 11:45 AM. Camera geometry and Image Alignment (Ivan Laptev and Josef Sivic).
  • [L] 1:30 PM – 3:00 PM. Efficient visual search (Josef Sivic). Slides available here.
  • [L] 3:15 PM – 4:45 PM. Efficient visual search (Cordelia Schmid). Slides available here (ppt file) and here (pdf file).
• Wednesday, January 26
  • [L] 8:15 AM – 9:15 AM. Bag-of-features models for category-level classification (Cordelia Schmid). Slides available here (ppt file) and here (pdf file).
  • [L] 9:30 AM – 10:30 AM. Bag-of-features models for category-level
    classification (Cordelia Schmid)
  • [E] 10:45 AM – 11:45 AM. Bag-of-features models for category-level classification (Ivan Laptev, Cordelia Schmid and Josef Sivic)
  • [L] 1:30 PM – 2:30 PM. Category-level localization (Ivan Laptev). Slides available here.
  • [L] 2:45 PM – 3:45 PM. Category-level localization (Ivan Laptev)
  • [E] 4:00 PM – 5:00 PM. Category-level localization (Ivan Laptev and Josef Sivic)
• Thursday, January 27
  • [L] 8:15 AM – 9:15 AM. Motion and human actions (Ivan Laptev). Slides available here.
  • [L] 9:30 AM – 10:30 AM. Motion and human actions (Ivan Laptev)
  • [L] 10:45 AM – 11:45 AM. Motion and human actions (Ivan Laptev)
• Friday, January 28
  • [L] 8:15 AM – 9:15 AM. Supervised learning (Zaid Harchaoui)
  • [L] 9:30 AM – 10:30 AM. Supervised learning (Zaid Harchaoui)
  • [E] 10:45 AM – 11:45 AM. Supervised learning (Zaid Harchaoui)

Total hours: 18 hours of lectures + 6 hours of practical exercises.

Prerequisites

The course is self-contained.

Bibliography

• D.A. Forsyth and J. Ponce, “Computer Vision: A Modern Approach, Prentice-Hall, 2003.
• J. Ponce, M. Hebert, C. Schmid, and A. Zisserman, “Toward category-level object recognition”, Springer LNCS, 2007.
• R. Szeliski, “Computer Vision: Algorithms and Applications”, Springer, 2010.
• O. Faugeras, Q.T. Luong, and T. Papadopoulo, “Geometry of Multiple Images,” MIT Press, 2001.
• R. Hartley and A. Zisserman, “Multiple View Geometry in Computer Vision”, Cambridge University Press, 2004.
• J. Koenderink, “Solid Shape”, MIT Press, 1990.

Registration

There are no registration fees. For organization reasons it is however necessary to register online; see the registration page.

Location and schedule

All the lectures will take place in “amphithéatre B”, at the 3rd floor of the GN1 building (main building of the “exact sciences” part of ENS Lyon, a.k.a. Campus Jacques Monod).

Local organizers

• Nicolas Brisebarre
• Guillaume Hanrot
• Jean-Michel Muller

There are several useful informations on the main page of the research schools in Computer Science at ENS Lyon.

Separation logic is an extension of Floyd-Hoare logic that makes it possible to reason about programs manipulating pointers. Since its introduction at the beginning of this millenary, it has led to several developments, which include tools for the automatic verification of properties of pointer manipulating programs, as well as reasoning about concurrent programs in a shared memory scenario.

This research school will take place in the week Jan.31st-Feb. 4, 2011.

Courses will be taught in english.

Slides:

HYang, intro, sep-logic, hiding, automation

AGotsman, concurrency, csl, lockfree, scheduler

MParkinson,abstract predicates, rely-guarantee, RGSep, deny-guarantee

Code: reverse.c, create.c, dispose.c, push.c, pop.c

The lecture notes on Separation Logic, written by J. Reynolds and mentioned by H. Yang in his lecture, are available here.

The prerequisite to follow the course is a basic knowledge of first-order logic.

Tool exercises: we suggest that attendees bring a laptop for the sessions devoted to tool exercises. Exercises will be made using the Verifast Program Verifier (follow the link to download and install the tool on your computer).

Lecturers

• Hongseok Yang (Lecturer, Queen Mary University of London, UK)
• Alexey Gotsman (Assistant Professor, IMDEA, Spain)
• Matthew Parkinson (Researcher, Microsoft Research, Cambridge, UK)

Topics (tentative description)

1) Basic separation logic.

• [a] Basic proof rules and semantics of separation logic.
• [b] Basic automatic verification algorithms based on separation logic.

2) Logic-based approaches on information hiding and data abstraction.

• [a] Higher-order frame rules and abstract predicates.
• [b] Automatic verification algorithm with abstract predicates.

3) Invariant-based approaches on the verification of concurrent programs.

• [a] Concurrent separation logic.
• [b] Automatic verification algorithm based on concurrent separation logic.

4) Rely-Guarantee.

• [a] RGSep: the marriage of rely-guarantee and separation logic.
• [b] Automatic verification with RGSep.
• [c] Reasoning about liveness properties.
• [d] Deny Guarantee.

Tentative schedule for the week. [L] means a lecture, and [E] means an exercise session.

Mon (5 hours)

• [L] Introduction and basic semantics (HY)     10h30
• [E] Introduction and basic semantics (HY)
• [E] Concurrent programming (AG)      14h00
• [L] Basic separation logic (HY)
• [E] Basic separation logic (HY)

Tue (5 hours)

• [L] Abstract predicate (MP)     9h00
• [E] Abstract predicate (MP)
• [E] Tool exercise 1 (AG)
• [L] Information hiding (HY)   14h00
• [E] Information hiding (HY)

Wed (7 hours)

• [L] Concurrent separation logic (AG)     9h00
• [E] Concurrent separation logic (AG)
• [E] Tool exercise 2 (AG)
• [L] RGSep (MP)              13h30
• [E] RGSep (MP)
• [L] Automation (HY)     16h00
• [E] Automation (HY)

Thu (4 hours)

• [L] Soundness of concurrent separation logic (AG)        9h00
• [L] Deny/Guarantee (MP)
• [E] Deny/Guarantee (MP)
• [L] ..

Fri (3+1 hours)

• [L] Liveness (AG)          9h00
• [E] Liveness (AG)
• [L] Concurrent abstract predicate (MP)
• Exam     (end: 13h00)

Please contact Daniel Hirschkoff if you have any question regarding this course.