16 Mars - 22 Mars


Retour à la vue des calendrier
Mardi 17 Mars
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: ALEA, au CIRM (16-20 mars)
Description: Journées ALEA
Jeudi 19 Mars
Heure: 12:15 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Calcul efficace de la stabilité des concepts formels
Description: Sadok BEN YAHIA Dans l'ère des données massives, l'alliance de la qualité avec l'efficience pour la sélection des concepts formels « intéressants » serait une condition sine qua non. Dans ce cadre, la mesure de stabilité, de concepts formels, indiquerait dans quelle mesure l'intension de ce concept est liée à la présence d'objets particuliers dans son extension. Un concept stable possède, ainsi, une existence d'autant plus « réelle » que son intension ne dérive pas fortuitement d'une description bruitée de ses objets. Ainsi, les concepts stables sont très intéressants à localiser dans beaucoup de domaines puisqu'ils sont résistants au bruit, e.g., détection de communautés stables, classification par des classes monothétiques/ polythétiques.

Cependant, le calcul de la stabilité serait très couteux, ie., exponentiel en fonction de la taille de l'extension du concept. En effet, il faudrait explorer l'espace de tous les sous-ensembles de l'extension à la recherche qui restent fidèles à l'intension du concept formel.

Dans ce séminaire, nous passons en revue les très peu nombreux travaux qui se sont intéressés au calcul de la stabilité des concepts formels (organisés sous forme de treillis ou non). Ensuite, nous présentons des travaux récents sur l'exploitation des propriétés de monotonie et d'anti-monotonies des éléments clés dans l'espace de recherche. Ainsi, la saturation des cliques maximales non génératrices permet de traiter des espaces avoisinant les 215000. Nous montrons aussi que les identités d'inclusion/ exclusion servent au calcul efficace des stabilités des concepts formels organisés sous la forme d'un treillis.
Heure: 14:30 - 15:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Effective verification of low-level software with nested interrupts
Description: Lihao Liang Interrupt-driven software is difficult to test and debug, especially when
interrupts can be nested and subject to priorities. Interrupts can arrive
at arbitrary times, leading to an explosion in the number of cases to be
considered. We present a new formal approach to verifying interrupt-driven
software based on symbolic execution. The approach leverages recent
advances in the encoding of the execution traces of interacting, concurrent
threads. We assess the performance of our method on benchmarks drawn from
embedded systems code and device drivers, and experimentally compare it to
conventional formal approaches that use source-to-source transformations.
Our experimental results show that our method significantly outperforms
conventional techniques. To the best of our knowledge, our technique is the
first to demonstrate effective formal verification of low-level embedded
software with nested interrupts.

Joint work with
Daniel Kroening, Tom Melham, Peter Schrammel and Michael Tautschnig
Vendredi 20 Mars
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: An infinitary model of linear logic
Description: Charles Grellois We construct an infinitary variant of the relational model of linear logic, where the exponential modality is interpreted as the set of finite or countable multisets. We explain how to interpret in this model the fixpoint operator Y as a Conway operator alternatively defined in an inductive or a coinductive way. We then extend the relational semantics with a notion of color or priority in the sense of parity games. This extension enables us to define a new fixpoint operator Y combining both inductive and coinductive policies. We conclude by sketching the connection between the resulting model of lambda-calculus with recursion and higher-order model-checking.