Colloquium

Situated interaction and co-adaptive systems: creating a partnership between people and intelligent systems

Mackay

Computer Science developed as a field at a time when computers were expensive, isolated machines run by teams of highly trained engineers. Not surprisingly, the primary focus of Computer Science has been on the computers themselves: how to make them faster, smarter and more efficient. However, computing has changed radically over the past two decades. Computers take many forms and are now ubiquitous, used in ways never imaged by the founders of the field.
My goal in this talk is to shift our perspective on computing: Rather than focusing on how to make computers smart, the question is how to use computers to make people smart. The foundations of Human-Computer Interaction build upon our understanding of memory, motor and perceptual skills, allowing us to create interactive systems that augment human capabilities. We are developing a new line of research that creates effective partnerships between people and computers, taking advantage of their respective strengths and minimizing their weaknesses. I will illustrate our approach with a variety of examples, including how we enhance creativity for contemporary music composers, support biologists as they manage large quantities of physical and electronic data, and even help distributed families to stay in touch.

Comment faire confiance à un compilateur ?

Leroy

Les outils de vérification formelle de programmes (analyseurs statiques, prouveurs de programmes, model-checkers) ont fait des progrès remarquables ces dernières années et commencent à percer dans le monde du logiciel critique. Cependant, ces outils ne vérifient "que" des programmes source: des erreurs dans les compilateurs qui les transforment en code machine exécutable ou dans les processeurs qui les exécutent peuvent toujours invalider les garanties obtenues par vérification du source. Je présenterai un projet en cours, appelé Compcert, qui vise à éliminer totalement cette incertitude dans le cas des compilateurs. Il s'agit d'un compilateur réaliste pour le sous-ensemble "embarqué critique" du langage C qui s'accompagne d'une preuve mathématique de préservation sémantique, montrant que le compilateur ne va jamais introduire d'erreurs dans le programme qu'il compile. Nous utilisons l'assistant de preuve Coq non seulement pour conduire cette preuve, mais aussi comme langage de programmation pour écrire le compilateur lui-même. Je terminerai par quelques perspectives plus générales sur l'avenir des langages et outils de programmation vus sous l'angle de la vérification formelle de programmes.

Modelling evolutionary games

Cannings

The notion of an ESS (evolutionarily stable strategy) was introduced by Maynard Smith and Price(1973) in order to provide an explanation for the co-existence of disparate strategies observed in fights between animals.
In some population individuals engage in pairwise contests using strategies drawn from some repertoire S. An individual who plays u ? S against one who uses v ? S receives a payoff E(u, v). Payoffs are additive so that an individual (or a group of individuals) using strategies according to some probability vector (or density) q say, in a population playing p receives E(q, p), the appropriate expectation. A strategy p is said to be an ESS if for any q p either (1) E(p, p) > E(q, p) or (2) E(p, p) = E(q, p) and E(p, q) > E(q, q). These conditions ensure that in some sense a population playing p is not invadable by any alternative.
There are some problems with the notion of an ESS. There is no well defined dynamic for the frequencies with which the strategies are played, and transmitted to subsequent generations. There is often no temporal framework within which the conflicts occur. These issues will be briefly discussed before moving on to discuss variants of one of the key models in the theory.
In the original model of the War of Attrition (Maynard Smith, 1974) individuals choose their strategies, which are times to display, from S = [0, ?). The contest continues until one of the individuals reached his chosen time and retreats, leaving the other as the winner to collect the reward V . Thus if x is played against y the payoff E(x, y) = V ?(x, y) ? min(x, y) where ?(x, y) = 1, 0.5, 0 for x >, =, < y respectively. The ESS is simple, it is given by the negative exponential density with mean V . There are many variants of this model (1) embedding it within some ecological framework, (2) embedding it with some temporal framework with variable rewards, (3) allowing multiple players and multiple rewards. We shall explore some of these and what they tell us about ESSs in general, as well as some new models.

Théorie de linformation : modèles, algorithmes, analyse

Vallée

Tout étudiant dun cours dalgorithmique de base apprend que la complexité moyenne de lalgorithme QuickSort est en O(n log n), celle de QuickSelect est en O(n) et celle de RadixSort est en O(n log n). De tels énoncés ont le mérite dêtre simples, mais leur simplicité est trompeuse, car ils sont fondés sur des hypothèses spécifiques à chaque algorithme : pour les deux premiers algorithmes, le coût unitaire est la comparaison entre clés, tandis que, pour le troisième, le coût unitaire est la comparaison entre symboles.
Ces études soufrent donc de deux inconvénients majeurs : il nest pas possible de comparer réellement ces algorithmes entre eux, car les mesures de coût sont différentes. Ensuite, la mesure de coût adoptée pour analyser QuickSort ou QuickSelect est peu réaliste, dès que les clés ont une structure complexe, ce qui est le cas dans le contexte des bases de données ou de la langue naturelle, par exemple.
Pour effectuer une analyse réaliste, il faut donc dabord travailler en théorie de linformation pour définir un cadre adapté. En théorie de linformation, une source est un mécanisme aléatoire qui produit des symboles dun alphabet donné. On construit ici un modèle de source très général, qui prenne en compte la possibilité de corrélations importantes entre symboles émis. Les clés considérées par lalgorithme sont alors des mots produits (indépendamment) par la même source.
Il faut ensuite considérer un coût unitaire qui soit le même pour tous les algorithmes : cest la comparaison entre symboles, et le coût de lalgorithme est donc le nombre total de comparaisons effectuées entre symboles.
Nous revisitons ainsi, dans un tel modèle, à la fois unifié et réaliste, lanalyse probabiliste de trois principaux algorithmes : QuickSort, QuickSelect, et les algorithmes de dictionnaire fondés sur la structure de tri.
Cet exposé est fondé sur des travaux communs avec Julien Clément, James Fill, et Philippe Flajolet.

Dynamic Local Remeshing for Elastoplastic Simulation

Shewchuk

We present a tetrahedral mesh improvement program called Stellar that locally optimizes finite element meshes so their worst tetrahedra have a level of quality substantially better than those produced by any previous method for tetrahedral mesh generation or "mesh clean-up." Our implementation usually improves meshes so that all dihedral angles are between 34 and 131 degrees.
We adapt our algorithms to the problem of dynamic remeshing to simulate a physical domain that is substantially reshaped by plastic flow or fracture. Our dynamic mesher is conservative: it replaces as few tetrahedra as possible, and thereby limits the visual artifacts and artificial diffusion that would be introduced if we repeatedly remeshed the domain from scratch. It also locally refines and coarsens a mesh, and even creates anisotropic tetrahedra, wherever a simulation requests it. Our simulation method addresses a range of material behavior from purely elastic to highly plastic, with particular advantages for objects that span both extremes at once. We illustrate these features with animations of elastic and plastic behavior, extreme deformations, and fracture.
Jonathan Shewchuk is an Associate Professor in the Department of Electrical Engineering and Computer Sciences at UC Berkeley. He is best known for his software Triangle for high-quality triangular mesh generation, which won the 2003 James Hardy Wilkinson Prize in Numerical Software, and his "Introduction to the Conjugate Gradient Method Without the Agonizing Pain."

Limitations and Tradeoffs ofg High Resolution LM Techniques

Pawley

As reviewed in the January, 2009 issue of Nature: Methods , the past decade has seen an explosion of fluorescence LM techniques demonstrating spatial resolution significantly beyond the Abbe Limit (HRLM). Are we truly on the verge of nm spatial resolution in living cells? Wonderful though these techniques are, I think that they will only be used in an optimal manner once their various limitations are better understood. Although they have sidestepped the diffraction limit, Poisson statistics still represents a significant barrier. Higher resolution implies smaller pixels and therefore the same (or greater) number of photons must originate from ever-smaller volumes of the specimen. More signal implies more phototoxicity. While no HRLM technique is free from limitations, each has a different suite of problems. It is the aim of this contribution to list and contrast the limitations, with an eye to determining which method is best suited to a particular type of structural investigation.
STORM and PALM rely on being able to image individual dye molecules sequentially using widefield fluorescence, to calculate and store the centroid of each diffraction-limited spot, and then to bleach or photodeactivate these molecules before imaging others. As in an earlier image-intensifier system developed for the EM , the final image is built up by summing the centroids from many (~1,000s) EM-CCD images, a process that takes some time. For this approach to work, signal from endogenous fluorophors must be kept very low, a requirement often satisfied by employing TIRF imaging. As a result, PALM and STORM are most suitable for imaging biological structures located very close to the coverslip surface. These imaging techniques also rely on photobleaching or photoswitching, processes that may also produce reactive oxygen species that can diffuse µm before reacting possibly with molecules that are not dyes.
On the other hand, the specimen is never subjected to the extreme energy density present in the STED beam. This high energy density may be the reason that most STED studies employ unfamiliar fluorophors that often emit in the red or near-IR. Despite this, STED can record 3D HRLM images at up to 28fps . Techniques using coherently structured-illumination such as 4Pi, and SIM, employ somewhat lower illumination intensities but they also require that the specimen be sufficiently optically homogeneous to preserve the geometric integrity of the illumination and imaging interference patterns, a condition not always easily met . Saturated widefield techniques, such as SSIM, expose the specimen to very high peak power levels and the low illumination duty cycle implies a data rate too slow for imaging moving specimens.

Simulation numérique pour la science des matériaux : vers une mécanique moderne

Le Bris

Les simulations numériques forment aujourd’hui une part grandissante de la science des matériaux. La mécanique du 19 eme siècle s’intéressait aux échelles du mètre et du millimètre, celle du vingtième à l’échelle du micromètre. Celle de ce siècle descend jusqu’au nanomètre. A de telles échelles, les phénomènes de chimie quantique, et les phénomènes atomistiques se couplent intimement aux effets macroscopiques. L ’exposé présentera ce que les mathématiques et la simulation numérique peuvent apporter, sur le cas de deux exemples particuliers: la mécanique des matériaux cristallins, et la rhéologie des fluides complexes (non Newtoniens). On illustrera notamment l’apport d’une théorie mathématique rigoureuse de passage au macroscopique, et celui d’une approche de simulation numérique multi-échelle.

Development of self-driving car for the DARPA urban challenge

Teller

In May 2006 we formed a team to compete in DARPA's 2006-2007 "Urban Challenge," the goal of which was to develop a passenger vehicle capable of safe, robust autonomous driving in city traffic. Over the following eighteen months, we built the team up to roughly twenty-five members, acquired more than a half-million dollars worth of sensors and mobile computers and data storage systems, assembled two autonomous vehicles, wrote (and discarded) hundreds of thousands of lines of new code, and tested our system extensively in various closed and public road networks around the country.
This talk surveys some of the issues that arose in the project, including systems design, sensor choice, environment/surround representation, codification of driving rules, algorithm development, testing methods, and safety. We'll show lots of real data, and examples of our algorithms doing reasonable and not-so-reasonable things. We will describe our experiences through the final stages of the competition. Finally, we'll attempt to identify some of the lessons we learned from the project. In particular, we will contrast two divergent approaches to the development of autonomous vehicles emerging from the robotics community: one centered on persistent data infrastructure, the other on just-in-time mobile sensing.

Près de 40 ans après le théorème de Cook, où en est la complexité algorithmique

Koiran

La notion de problème NP-complet a connu un succès extraordinaire dès son introduction au début des années 1970.
Très rapidement, des centaines puis probablement des milliers de problèmes NP-complets ont été identifiés.
Aujourd'hui, même si la preuve de NP-complétude d'un nouveau problème peut parfois présenter des difficultés techniques non négligeables, cette notion est utilisée de manière quasiment routinière pour justifier l'absence d'algorithme polynomial pour des problèmes issus de pratiquement tous les domaines de la science et de la technologie.
Malheureusement, tous ces résultats ne reposent pas sur une base bien solide puisqu'on ne sait pas démontrer que les problèmes NP-complets n'admettent pas d'algorithme polynomial. En effet, près de 40 ans après son introduction le problème "P=NP ?" reste largement ouvert.
Sans prétendre à l'exhaustivité, je ferai un petit historique de cette question et je présenterai quelques unes des approches qui ont été proposées pour aborder le problème "P=NP ?" et des problèmes voisins.

Point-clouds, sensor networks, and persitence: algebraic topology in the 21st century

De Silva

Ever since the discovery and publication of the persistent homology algorithm, by Edelsbrunner, Letscher and Zomorodian in 2000, classical algebraic topology has enjoyed new life as a field of applied mathematics. Whereas algebraic topology has traditionally been regarded as a technically complex and challenging discipline, the underlying geometric intuitions are very natural. In the 21st century, these beautiful ideas are accessible to anyone: large experimental data sets provide a rich source of examples, while powerful computers carry out the necessary homological algebra. I will discuss several modern applications of algebraic topology, from nonlinear statistics to sensor networks. The talk is intended for a general audience.