Model-checking is a approach to formal verification whose goal is to automatically establish the validity of a certain specification over the system under study. Generally, the system is modelled as an automaton of some kind, whereas the specification is described as a logical formula. To formalize the specification of temporal properties, temporal logics are the most accepted tool.

After a (long) introduction to classical temporal logics (LTL and CTL), we will see how adding new counting operators to these logics allows us to specify more easily and concisely a certain number of properties. Finally, I will present shortly the various complexity results we obtained on the model-checking problem of these extensions, compared to the classical ones.

In case logic tends to make you run away, don't worry, in most of the talk we will try to understand examples and see what you can express with simple logic tools.

On fera d'abord une courte introduction à la sémantique des jeux. Celle-ci consiste à décrire les programmes d'un certain type par des stratégies sur un certain jeu; l'environnement d'un programme étant considéré comme son adversaire. Les termes du lambda-calcul ne décrivent pas toutes les stratégies, mais uniquement celles qui sont "innocentes", c'est à dire (essentiellement) celle qui réagissent de la même manière lors d'appels successifs. Le lambda lambda-bar calcul, en introduisant la possibilité de modifier la valeur d'un argument déjà passé, permet de décrire des stratégies non innocentes. Cette extension donne donc une représentation syntaxique de ce qu'est "naturellement" la sémantique des jeux.

Proof-nets are a graphical language originated from Linear Logic that, in some very limited cases, can substitute sequent calculi allowing a graph-theoretical approach to logic. Unfortunately, they are a rather exotic formalism, with no fundamental text, many variants and many "dark sides" which are mostly part of folklore. I dedicated my phd to the understanding of their problems and in this talk I would try to give an introduction to the subject, starting with the easiest case of proof nets for multiplicative linear logic without constants, and hoping to give some new insights coming from my research work. After having introduced the basics, I shall discuss correctness criterions, i.e. sound and complete graph-theoretical abstraction of a given logic. Time permitting, I shall discuss some of the problems/extensions of the theory. No previous knowledge of Proof-Nets, nor of Linear Logic, is required. The presentation will be informal and, hopefully, interactive.

(exposé en français)

We define a logic, called CSL, for the specification of complex data structures, and we show its use in program verification. Our framework allows to handle programs with dynamic linked structures and arrays carrying unbounded data, as well as the composition of these structures. The formulas in CSL allow a limited form of alternation between existential and universal quantifiers and they can express (1) constraints on reachability between positions in the heap following some pointer fields, (2) linear constraints on the lengths of the lists and the indexes of the arrays, and (3) constraints on the values of the data attached to these positions. For data constraints, the logic CSL is parameterized by a first-order logic over the considered data domain. We prove that the satisfiability problem of CSL is decidable whenever the underlying data logic is decidable and that CSL is closed under the computation of the strongest post-condition in the considered class of programs.

Les classes de permutations sont des objets combinatoires étudiés aussi du point de vue algorithmique. Elles ont été introduites par D. Knuth en 1973 pour décrire les permutations triables par différentes méthodes, par exemple l’ensemble des permutations triables par une pile est la classe des permutations évitant le motif 231, et cette classe est dénombrée par les nombres de Catalan (elle est en bijection avec les mots de Dyck). Il est naturel de chercher à étendre ces résultats de dénombrement à toutes les classes, mais jusqu'à présent peu de résultats généraux ont été établis.

Après une introduction aux problématiques combinatoires et algorithmiques sur les classes de permutations, je présenterai un algorithme utilisant les permutations en épingles et la théorie des automates pour décider si une classe de permutations contient un nombre fini de permutations simples. Pour ceux qui pensent que la combinatoire se résume à d'affreux calculs et de grosses formules, n'ayez crainte : dans cet exposé il n'y aura aucun calcul et aucune formule, seulement d'astucieux résultats et de jolis dessins de permutations en épingles !

Faire jouer les ordinateurs à divers jux a depuis longtemps servi à mesurer les avancées dans le domaine de l'intelligence artificielle. Les échecs et d'autres jeux déterministes - jeux sans hasard, et où l'état du jeu est connu parfaitement par l'ensemble des joueurs - en ont été un exemple récent. Cependant, ans la plupart des situations réelles interviennent un élément de hasard et certaines informations ne sont pas partagées entre les acteurs. Le poker, joué par des millions de personnes dans le monde, fait intervenir ces contraintes. La recherche sur le poker a fait l'objet de nombreuses avancées ces dernières années, si bien que les programmes actuels sont au niveau des meilleurs joueurs mondiaux en 1 contre 1 (head's up), malgré la NP-complétude du problème. L'exposé présentera les grandes lignes du sujet, les approches récentes, et cherchera à développer l'intuition sur la complexité des problèmes rencontrés. Une connaissance même succinte des règles du poker Texas Hold'em contribuera à une compréhension plus agréable de l'exposé.

En finance, connaissant un état présent il est important d'avoir une idée de l'état futur (à court et si possible long terme). Il existe de nombreux modèles permettant d'expliquer ce futur. Le plus connu (et le moins utilisé à l'heure actuelle) étant le modèle de Black et Scholes.

Après une brève introduction au langage financier, nous verrons comment créer des modèles simples puis plus complexes collant à nos données. Nous nous attarderons enfin sur la résolution du futur, que ce soit en passant par une formule fermée si on a de la chance, ou par une simulation Monte Carlo.

Un point final sera donné sur les limitations des modèles utilisés, conséquences souvent immédiates de limitations techniques due à des temps de calcul trop importants.

Il ne sera pas fait état de la crise des subprimes de 2007 dont on subit les conséquences aujourd'hui à travers la crise financière d'envergure mondiale ; ni même de ses origines dans des produits financiers complexes tels que les CDS...

Dans le cas des langages de mots, il est équivalent d'être reconnu par automate ou par semigroupe fini, et on dispose de belles caractérisations de certaines classes (théorème de Schützenberger par exemple). On va ici étudier une extension quantitative de ces modèles.

On remplace les langages, où un mot est soit accepé soit refusé, par les fonctions de coût, qui attribuent une valeur entière à chaque mot. Comme dans le cas des langages, on pourra calculer des fonctions de coût au moyen d'automates ou de semigroupes, ces objets étant des extensions de ceux utilisés dans la théorie standard (on les appellera respectivement automates de coût et semigroupes de stabilisation). Ces fonctions de coût seront également dites "régulières"

Si on a le temps, on verra une caractérisation d'une classe intéressante de fonctions de coût via les automates de coût d'une part et les semigroupes de stabilisation d'autre part, à la manière de Schützenberger.

Ecrire un programme concurrent (c'est-à-dire qui fait plusieurs choses à la fois) est notoirement difficile. Les programmeurs médiocres utilisent des threads. Les bons programmeurs les utilisent bien. Les programmeurs chevronnés utilisent des événements. Les programmeurs fonctionnels, enfin, utilisent la monade des continuations.

Et si l'on mettait tout le monde d'accord ? « Threads, continuations et cotillons » vous montrera, par l'exemple, comment transformer automatiquement des threads en événements, grâce à la magie des continuations. Sans aucun truquage, nous irons même voire sous le capot comment implémenter tout ça pour le langage C. Sous vos yeux ébahis, resplendira alors CPC.

Quel rapport entre un réseau de téléphones portables, le pass navigo et des puces de détection de la grippe aviaire ? Non, pas de machination, mais des structures dans lesquelles des puces électroniques sont capables de communiquer entre elles dans un certain voisinage, d'effectuer localement de petits calculs mais ne maîtrisent pas la façon dont elles se déplacent (elles suivent leur porteur qui est généralement animé d'une volonté propre). Ces réseaux de communication dépendants d'un voisinage géographique et qui évoluent en permanence sont appelés réseaux sociaux opportunistes.

En 2004 un modèle a été introduit par Angluin et al. pour décrire et comprendre le comportement de certains réseaux de ce type : les protocoles de population dans lesquels les agents sont en plus anonymes et indistinguables. Comment, alors, faire des calculs globaux à l'aide d'informations sur un environement local qui change en permanence ? Comment ces systèmes se comportent ils lorsqu'on envisage une population si grande qu'elle en devient infinie ?

C'est à ce genre de questions que j'essaierai d'apporter des éléments de réponse formels en présentant le modèle d'Angluin et une extension vers des très grandes populations. Avec des vrais morceaux de calculabilité, d'arithmétique de Presburger, de probas et, si vous êtes sages, la racine carrée de 1/2.

Un effet dans un programme est une opération qui modifie l'état du système, comme l'écriture d'une référence ou l'envoi d'un message dans un canal. Les systèmes de types traditionnels (ML) ignorent complètement ce genre d'opérations (je crois qu'elles ne leur font aucun effet) et il est du coup possible de typer des programmes qui divergent.

Je profiterai donc de cet exposé pour vous expliquer qu'il n'y a pas de raison de paniquer en vous introduisant les systèmes de types et effets. On verra comment l'état du système s'organise en un ensemble de régions permettant de simuler des concepts familiers comme les références ou les canaux. Puis j'introduirai la condition de stratification sur les régions qui permet de retrouver la propriété de terminaison des programmes typables. Enfin, si le temps le permet, on parlera de quelques raffinements possibles permettant, par exemple, de traiter de confluence...