Jeudi 6 Novembre
Heure: |
16:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Introduction to Partial Order Reductions |
Description: |
César Rodríguez In model checking, a well known source of state-space explosion (SSE) is the explicit representation of concurrent actions by their interleavings. Partial-order reductions (PORs) are a family of techniques attempting to cope with this by constructing an equivalent state space where irrelevant executions of the original are discarded.
This talk will be a gentle introduction to the topic. We will focus on Godefroid's persistent sets, prove that a selective exploration based on them visits all deadlocks, discuss the two main classes of algorithms for computing them, and finish, time permitting, with an overview of the conceptual similarities and differences between PORs and the unfolding technique. |
Mardi 18 Novembre
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Cryptophie : Black-box Trace and Revoke Codes |
Description: |
Phan Duong Hiuu |
Jeudi 20 Novembre
Heure: |
15:30 - 16:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Abstraction and Modular Verification of Services Using Symbolic Observation Graph (SOG) |
Description: |
Hanene Ochi For automatically composing services in a correct manner, information about their behaviors (an abstract model) has to be published in a repository. This abstract model must be sufficient to decide whether two, or more, services are compatible (the composition is possible) without including any additional information that can be used to disclose the privacy of these services. The compatibility between two services can be based either on some generic properties or specific ones . This talk will present my work during my thesis about the problem considering these kinds of compatibility criteria, and we will introduce approches for the automatic abstraction of services and to the modular checking of their compatibility using their abstract models only. To abstract services, we use the symbolic observation graph (SOG) approach that preserves necessary informa tion for service composition and hides private information. We will show how the SOG can be adapted and used so that the verification of generic and specific compatibility criteria can be performed on the composition of the abstract models of services instead of the original composite service. |
Vendredi 21 Novembre
Heure: |
10:30 - 12:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Chemins en ludique non-linéaire |
Description: |
Alice Pavaux La ludique est une théorie logique basée sur l'interaction, introduite il y a une quinzaine d'années par J.-Y. Girard. Elle s'inscrit dans un contexte marqué par les avancées importantes en théorie de la démonstration et en sémantique des langages de programmation permises par la logique linéaire. On se propose ici d'étudier les mécanismes de l'interaction dans une variante non-linéaire de la ludique, afin de poser les outils nécessaires à l'étude des types dans ce cadre. Cela se fera en décrivant les chemins suivis au cours de l'interaction au sein des desseins, les objets de la ludique. La non-linéarité permet de ne pas se restreindre au fragment multiplicatif-additif de la logique linéaire. |
Mardi 25 Novembre
Heure: |
14:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Le diamètre asymptotique des associaèdres généralisés |
Description: |
Lionel Pournin Les associaèdres généralisés ont été introduits par SergeyFomin et Andrei Zelevinsky dans le cadre de la théorie des algèbresamassées, et réalisés géométriquement par Chapoton, Fomin etZelevinsky. Ils sont associés à n'importe quel groupe de Coxeter fini.Parmi eux figurent trois familles infinies de polytopes : lesassociaèdres de type A (associaèdres usuels), de type B ou C(cycloèdres), et de type D.Le diamètre asymptotique des associaèdres de types A, B (ou C), et Dest maintenant connu et cet exposé passera en revue les cas des typesB (ou C), et D. Les preuves ne seront pas données entièrement, maisseulement esquissées. Quelques questions associées seront finalementdiscutées. |
Jeudi 27 Novembre
Heure: |
16:00 - 17:00 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
Precise Robustness Analysis of Real-Time Systems |
Description: |
Étienne André Quantifying the robustness of a real-time system consists in measuring the maximum extension of the timing delays such that the system still satisfies its specification. In this work, we introduce a more precise notion of robustness, measuring the allowed variability of the timing delays in their neighbourhood. We consider here the formalism of time Petri nets extended with inhibitor arcs. We use the inverse method, initially defined for timed automata. Its output, in the form of a parametric linear constraint relating all timing delays, allows the designer to characterise the system local robustness, and hence to identify the delays allowing the least variability. We also exhibit a condition and a construction for rendering robust a non-robust system. This work is a joint work with Laure Petrucci. |
Vendredi 28 Novembre
Heure: |
11:00 - 12:30 |
Lieu: |
Salle B107, bâtiment B, Université de Villetaneuse |
Résumé: |
New applications of moment-SOS hierarchies |
Description: |
Victor Magron Semidefinite programming is relevant to a wide range of mathematic fields, including combinatorial optimization, control theory, matrix completion. In 2001, Lasserre introduced a hierarchy of semidefinite relaxations for particular polynomial instances of the Generalized Moment Problem (GMP). My talk emphasizes new applications of this moment-SOS hierarchy, investigated during my PhD and Postdoc research.
In the context of formal proofs for nonlinear optimization, one can combine the moment-SOS hierarchy with maxplus approximation of semiconvex functions. Such a framework is mandatory for formal certification of nonlinear inequalities, occurring by thousands in the proof of Kepler Conjecture by Hales.
I also present how to approximate, as closely as desired, the Pareto curve associated with bicriteria polynomial optimization problems or the projections of semialgebraic sets. For each problem, one builds a hierarchy of semidefinite programs, so that the sequence of bounds converges in L1 norm.
Finally, this hierarchy allows to analyze programs containing loop invariants with polynomial assignments. |
|
|