Mardi 2 Décembre
Heure: 
12:30  13:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Robust network design with uncertain outsourcing cost 
Description: 
Michael Poss The expansion of a telecommunications network faces two sources of uncertainty, which are the demand for traffic that shall transit through the expanded network and the outsourcing cost that the network operator will have to pay to handle the traffic that exceeds the capacity of its network. The latter is determined by the future cost of telecommunications services, whose negative correlation with the total demand is empirically measured in the literature through the price elasticity of demand. Unlike previous robust optimization works on the subject, we consider in this paper both sources of uncertainty and the correlation between them. The resulting mathematical model is a linear program that exhibits a constraint with quadratic dependency on the uncertainties. To solve the model, we propose a decomposition approach that avoids considering the constraint for all scenarios. Instead, we use a cutting plane algorithm that generates required scenarios on the fly by solving linear multiplicative programs. Computational experiments realized on the networks from SNDlib show that our approach is orders of magnitude faster than the classical semidefinite programming reformulation for such problems. 
Heure: 
14:00  17:00 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Analyse en moyenne d'algorithmes sur les graphes 
Description: 
Vlady Ravelomanana 
Mardi 9 Décembre
Heure: 
12:30  13:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Complexity aspects of graph convexities 
Description: 
Mitre Dourado In the first half of the talk, I will survey the basic concepts, problems and main known results related to computational complexity aspects of graph convexities. In the second half, I will present some new results on the Radon number in the geodetic convexity, among them a polynomial time algorithm for finding the Radon number of unit interval graphs.
This is a joint work with: Jayme Luiz Szwarcfiter Alexandre Toman 
Heure: 
14:00  17:00 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Asymptotic expansion for random tensor models 
Description: 
Adrian Tanasa Threedimensional random tensor models are a natural generalization ofthe celebrated matrix models. The associated tensor graphs, or 3Dmaps, can be classified with respect to a particular integer orhalfinteger, the degree of the respective graph.I will present in this talk a combinatorial analysis of the generalterm of the asymptotic expansion in N, the size of the tensor, of aparticular random tensor model, the socalled multiorientable model.I will then present some enumerative results and show which are thedominant configurations of a given degree; several examples will alsobe given. 
Jeudi 11 Décembre
Heure: 
16:00  17:00 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
CosyVerif: An Open Source Extensible Verification Environment 
Description: 
Étienne André Over the past two decades, numerous verification tools have been successfully used for verifying complex concurrent systems, modelled using various formalisms. However, it is still hard to coordinate these tools since they rely on such a large number of formalisms. Having a proper syntactical mechanism to interrelate them through variability would increase the capability of eff ective integrated formal methods. Here, we propose a modular approach for defining new formalisms by reusing existing ones and adding new features and/or constraints. Our approach relies on standard XML technologies; their use provides the capability of rapidly and automatically obtaining tools for representing and validating models. It thus enables fast iterations in developing and testing complex formalisms. As a case study, we applied our modular definition approach on families of Petri nets and timed automata. This work is implemented in the CosyVerif platform, a modular framework integrating verification software tools of the Paris regions. This is a joint work with the CosyVerif team. 
Vendredi 12 Décembre
Heure: 
11:00  12:30 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Asynchronous Interaction with Theorem Provers: ProofGeneral's Last March 
Description: 
Carst Tankink This year ProofGeneral, the generic Emacsinterface for proof assistants, celebrates its 20th birthday. The tool is showing its age, however, by only allowing a user to work at a single point at the time, and having to reevaluate an entire proof script in reaction to changes at the beginning. In this talk, I will discuss our recent efforts to changing this situation: based on a previous endeavour in Isabelle, we have adapted the Coq proof assistant to work with the jEdit text editor. This editor has no uservisible notion of "State": the entire proof is always available to the proof assistant, allowing it to react to changes in the document in a more intelligent manner: by scheduling proofs in parallel and by postponing computation that are of no direct interest to the author. I will not go into full technical details in this talk, but give a demo of the current prototype, and discuss the ramifications of such a model in the longer term. 
Mardi 16 Décembre
Heure: 
14:10  17:00 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Plus long cycle dans les graphes aléatoires 
Description: 
Vlady Ravelomanana 
Heure: 
15:10  18:00 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Dependence and phase change in random mary search trees 
Description: 
HsienKuei Hwang 
Jeudi 18 Décembre
Heure: 
16:00  17:00 
Lieu: 
Salle B107, bâtiment B, Université de Villetaneuse 
Résumé: 
Teaching Formal Methods: Experience at UPMC and UP13 with CosyVerif 
Description: 
Laure Petrucci Nowadays, students are more and more demanding for practical coursework, which is a challenge when teaching formal approaches to software engineering. The solution is to provide environments for such handson sessions and homework, but this raises numerous difficulties. The environment must be: (i) multiplatform (Mac OS, Linux, Windows) so as to enable student practice at home, (ii) easy to deploy, (iii) easy to use and to take charge of, and (iv) flexible enough to enable the integration of new notations and associated services.
CosyVerif is a software environment dedicated to graphical notations, that provides the mechanisms and means for an easy integration of additional existing software for teaching (or demonstration) purposes. This makes it an interesting platform to establish new courses.
This paper presents our experience using CosyVerif for teaching Petri nets and parametric timed automata in two universities of the Paris region, i.e. Université Pierre et Marie Curie, and Université Paris 13. We also use CosyVerif to build demonstrators of Ph.D. students' work. 

