2017


Retour à la vue des calendrier
Mardi 3 Janvier
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Combinatorial physics, hypergeometric functions and symmetries of differential equations
Description: Youssef Abelaziz
Mardi 10 Janvier
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Algorithmes efficaces de génération aléatoire contrainte
Description: Philippe Duchon
Heure: 15:00 - 18:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Combinatorial physics, hypergeometric functions and symmetries of differential equations
Description: Youssef Abelaziz
Jeudi 12 Janvier
Heure: 13:00 - 14:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Harnessing Malware Intelligence for Defense and Attribution
Description: Arun Lakhotia The number of unique malware has been doubling every year for over two decades.
The majority of effort in malware analysis has focused on methods for
preventing malware infection. We view the exponential growth of malware as an
underutilized source of intelligence. Given that the number of malware authors
are not doubling each year, the large volume of malware must contain evidence
that connects them. The challenge is how to extract the connections and do so
in a timely manner to be useful.

This talk will describe Cythereal MAGIC, a cloud-based malware analysis
service, for mining large scale malware repositories. MAGIC, an offshoot of
research conducted under the DARPA Cyber Genome program, uses malware "genome"
to construct features that are resilient to many obfuscations. The correlations
discovered by MAGIC can be used to prevent and detect zero-day malware. The
correlations can also be used to investigate malware attacks for attribution.
Heure: 15:30 - 16:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Parametric model checking timed automata under non-Zenoness assumption
Description: Gia Real-time systems often involve hard timing constraints and concurrency, and are notoriously hard to design or verify. Given a model of a real-time system and a property, parametric model-checking aims at synthesizing timing valuations such that the model satisfies the property. However, the counter-example returned by such a procedure may be Zeno (an infinite number of discrete actions in a finite time), which is unrealistic. On the one hand, we show that synthesizing parameter valuations such that at least one counter-example run is non-Zeno is undecidable for Parametric Timed Automata (PTA). On the other hand, we propose a procedure based on a transformation of PTA into Clock Upper Bound PTA to derive such valuations.
Jeudi 19 Janvier
Heure: 15:30 - 16:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: What’s decidable about parametric timed automata?
Description: Étienne André Parametric timed automata (PTA) are a powerful formalism to reason,
simulate and formally verify critical real-time systems.
After two decades of research on PTA, it is now well-understood that
any non-trivial problem studied is undecidable for general PTA.
We provide here a survey of decision and computation problems for PTA.
On the one hand, bounding time, bounding the number of parameters or
the domain of the parameters does not (in general) lead to any decidability.
On the other hand, restricting the number of clocks, the use of
clocks (compared or not with the parameters), and the use of parameters
(e.g. used only as upper or lower bounds) leads to decidability of some
problems.
Mardi 24 Janvier
Heure: 12:30 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Reformulations for Mixed-Integer Nonlinear Programs: a surprisingly simple one with surprisingly good results in (quite) a few different applications
Description: Antonio Frangioni We describe a quite long line of research about the Perpective Reformulation of certain Mixed-Integer NonLinear Programs, which started with a total serendipity moment motivated by trying to prove wrong a referee who was in fact right but for the wrong reasons. The research was brought forward in part by a series of othe r developments motivated by factors such as the need to finding another application to publish the first paper, the need of fending off competing research teams, and finding a good idea as a by-product of an original one that would never work. All this brought us to a Project-and-Lift approach to certain projected reformulations of the Perspective Reformulation which seems to be one of the few authentic violations of the "no free lunch principle": an easy reformulation of a MIQP with the very same size and structure as the original one but with a substantially stronger bound. Apart from providing an overview on a recent and potentially interesting research field in MINLP, we hope that this talk can motivate the audience to making more errors and looking at them with more interest.
Jeudi 26 Janvier
Heure: 12:15 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Fouille de données déclarative
Description: Benjamin Negrevergne Une grande variété de techniques de fouille de données ne sont disponibles que sous la forme d'algorithmes en programmation impérative. Ces algorithmes sont difficiles à (ré-)utiliser et difficiles à adapter aux besoins de leurs utilisateurs. Une proposition récente vise à utiliser le paradigme de la programmation par contraintes pour obtenir des formulations plus déclaratives de ces techniques. Cette approche offre de nombreux avantages, comme celui de pouvoir incorporer facilement des connaissances métier au sein du processus de fouille.

Dans cette présentation, j'expliquerai comment formuler et résoudre efficacement des problèmes de fouille de données grâce à la programmation par contraintes. Je parlerai également des limites de cette approche pour la formulation de problèmes de fouille de données structurées (fouille de séquences ou graphes) ou par la formulation de critères d'intérêts complexes (combinaisons de contraintes, préférences) ainsi que de mes contributions dans ce domaine.
Mardi 31 Janvier
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Enumerative combinatorics of maps/polyominoes/2-stack-sortable permutations
Description: Veronica Guerrini
Jeudi 2 Février
Heure: 12:15 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Complétion de valeurs manquantes à l'aide d'un surfeur aléatoire
Description: François Rioult Dans les contextes réels, des valeurs manquantes figurent dans les données et il est possible d'obtenir des informations contextuelles expliquant l'absence de valeur : y-a-t-il une valeur spécifique pour un autre attribut ? y-a-t-il une autre valeur manquante ? etc. Ces informations contextuelles peuvent être organisées sous forme de graphe, où un surfeur aléatoire fera émerger l'explication la plus probable pour cette valeur manquante. Cette explication donne des indications sur une potentielle complétion.
Mardi 7 Février
Heure: 12:30 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Reformulations de programmes quadratiques convexes en nombres entiers
Description: Dominique Quadri La programmation quadratique en nombres entiers trouve de nombreuses applications dans le monde réel. Il semble important de développer des méthodes de résolution exactes permettant de résoudre en des temps CPU limités de tels problèmes. Or de nos jours les solveurs de programmation linéaire sont de plus en plus efficaces. C'est pourquoi cet exposé est axé sur des reformulations de programmes quadratiques en variables entières en programmes linéaires.
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Algorithmic geometry: growth rate and consequence on a generalization of Sauers's lemma (TBC)
Description: Xavier Goaoc
Jeudi 9 Février
Heure: 13:00 - 14:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Malware Detection Based On Graph Classification
Description: Khanh Huu The Dam Malware detection is nowadays a big challenge. The existing techniques for malware detection require a huge effort of engineering to manually extract the malicious behaviors. To avoid this tedious task of manually discovering malicious behaviors, we propose in this paper to apply learning for malware detection.
Given a set of malwares and a set of benign programs, we show how learning techniques can be applied in order to detect malware.
For that, we use abstract API graphs to represent programs. Abstract API graphs are graphs whose nodes are API functions and whose edges represent the order of execution of the different calls to the API functions (i.e., functions supported by the operating system). To learn malware, we apply well-known learning techniques based on Random Walk Graph Kernel (combined with Support Vector Machines). We can achieve a high detection rate with only few false alarms (98.93% for detection rate with 1.24% of false alarms).
Moreover, we show that our techniques are able to detect several malwares that could not be detected by well-known and widely used antiviruses such as Avira, Kaspersky, Avast, Qihoo-360, McAfee, AVG, BitDefender, ESET-NOD32, F-Secure, Symantec or Panda. This is a joint work with Tayssir Touili.
Vendredi 10 Février
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Syntaxe transcendentale: première lecture.
Description: Christophe Fouqueré JY Girard, avec ses 3 articles sur la "syntaxe transcendentale", aborde la logique sous un angle à la fois philosophico-logique et sous un angle technique, pour aller au-delà de ce qui est fait jusqu'à présent: non seulement la logique linéaire propositionnelle mais encore le traitement de l'égalité donc du premier ordre. Modestement, je commencerai par présenter la partie technique, qui reprend et étend le modèle des réseaux de preuves, en présentant la représentation de MALL et des exponentielles.
Mardi 14 Février
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Quantum simulation of a 2D quasicrystal with cold atoms
Description: Nicolas Macé
Lundi 20 Février
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: L’évolution des bases de connaissances RDF
Description: Fatma Chamekh En 2006, Tim Berners-Lee a présenté le web de données ou données liées (Linked data web of data) comme une nouvelle perspective du web sémantique. L'idée est de privilégier la publication des données structurées sur le web, sous forme d'un réseau global d'informations, en les reliant les unes aux autres. Cependant, des nouveaux jeux de données sont créés ou d’autres sont mises à jour. D’où, les bases de connaissances RDF ont besoin d’évoluer. Dans ce séminaire, je présenterai mes travaux de recherche qui porte sur l’évolution des bases de connaissances RDF en se focalisant sur la qualité des données et la gestion des versions. Dans un premier temps, j’exposerai mon travail de thèse. Il s’agit d’une approche pluridisciplinaire qui allie le paradigme agent aux technologies du web sémantique. Cette approche emploie les capacités cognitives et réactives des agents pour gérer la qualité des données et la gestion des versions. Dans un deuxième temps, je présenterai un bref aperçu sur mes travaux de recherche actuels.
Mardi 21 Février
Heure: 12:30 - 13:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: A Column Generation approach for a Multi-Activity Tour Scheduling Problem
Description: Stefania Pan
Heure: 13:00 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Simplicial Decomposition for Large-Scale Quadratic Convex Programming
Description: Enrico Bettiol
Vendredi 24 Février
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Expérimenter un modèle de programmation fonctionnel, réactif et concurrent (à environnement global) compositionnel en OCaml.
Description: Jean-Vincent Loddo Note: Il s'agit d'un groupe de travail informel et non d'une présentation.


Abstract:
OCaml est un langage nativement multi-paradigme, permettant un style de programmation fonctionnel, impératif et objet. Une librairie de processus légers (threads), fournie avec le langage et s'appuyant sur le système d'exploitation sous-jacent, permet d'ajouter à la liste précédente le style de programmation concurrent à mémoire partagée (ou environnement "global"). Or, cette variante du style concurrent paraît tellement difficile et source d'erreurs ("race conditions", "deadlocks", "resource starvation") qu'elle est souvent réputée impraticable. Ce constat a probablement influencé la recherche sur les paradigmes concurrents, qui s'est orientée, depuis la fin des années '70 et début '80, sur le modèle opposé des algèbres de processus, c'est-à-dire à environnement "local" ou échange de messages (CSP de Hoare 1985, CCS de Milner 1989, LOTOS ISO 1985). L'intérêt soulevé par les mémoires transactionnelles à partir des années 2000, témoigne toutefois d'un retour à la mode de l'environnement global dans un cadre de programmation multi-thread.

Entre-temps, un autre style de programmation, très adapté aux programmes interactifs et typiquement avec interface graphique, le style "réactif" (ou programmation événementielle) a fait brèche dans la culture des programmeurs et le support de ce style est offert dans un nombre grandissant de langages "mainstream", impératifs ou fonctionnels.

Tout cela peut s'ajouter et se combiner à l'ancienne notion de "promesse" ("future") proposée comme mécanisme de synchronisation de programmes hybrides fonctionnels-concurrents (Friedman & Wise 1976, Baker & Hewitt 1977).

Dans cet exposé nous présenterons une tentative de synthèse des styles fonctionnel, réactif et concurrent à environnement global, qui soit compositionnelle, c'est-à-dire permettant de composer des éléments modulaires. Cette solution, qui prend la forme contingente d'une librairie OCaml, a été inspirée par l'implémentation courante du logiciel Marionnet (simulateur de réseaux TCP/IP) et devrait, à terme, permettre la ré-implantation d'une partie critique du code.
Jeudi 2 Mars
Heure: 12:30 - 13:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: On big data, optimization and learning
Description: Prof. Andrea Lodi In this talk I review a couple of applications on Big Data that I personally like and I try to explain my point of view as a Mathematical Optimizer -- especially concerned with discrete (integer) decisions -- on the subject. I advocate a tight integration of Machine Learning and Mathematical Optimization (among others) to deal with the challenges of decision-making in Data Science. For such an integration I try to answer three questions: 1) what can optimization do for machine learning? 2) what can machine learning do for optimization? 3) which new applications can be solved by the combination of machine learning and optimization?
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Reachability Analysis of Pushdown Systems with an Upper Stack
Description: Adrien Pommellet Pushdown systems (PDSs) are a natural model for sequential programs, but they can fail to accurately represent the way an assembly stack actually operates. Indeed, one may want to access the part of the memory that is below the current stack or base pointer, hence the need for a model that keeps track of this part of the memory. To this end, we introduce pushdown systems with an upper stack (UPDSs), an extension of PDSs where symbols popped from the stack are not destroyed but instead remain just above its top, and may be overwritten by later push rules.

We prove that the sets of successors post* and predecessors pre* of a regular set of configurations of such a system are not always regular, but that post* is context-sensitive, so that we can decide whether a single configuration is forward reachable or not. In order to underapproximate pre* in a regular fashion, we consider a bounded-phase analysis of UPDSs, where a phase is a part of a run during which either push or pop rules are forbidden. We then present a method to overapproximate post* that relies on regular abstractions of runs of UPDSs. Finally, we show how these approximations can be used to detect stack overflows and stack pointer manipulations with malicious intent.
Vendredi 3 Mars
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Introduction à la théorie de la complexité géométrique, d'après K. Mulmuley
Description: Luc Pellissier La théorie de la complexité géométrique est un programme de recherche porté par
Ketan Mulmuley, qui vise à résoudre des questions de complexité après les avoir
traduites comme des inclusions de surfaces algébriques représentant des groupes
de symétries.

Après avoir présenté la théorie avec beaucoup de recul, on présentera un
résultat de séparation obtenu ainsi (entre P et une classe ad hoc).
Lundi 6 Mars
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Automatic Deception Detection in Text Applying Topic Modeling Algorithms
Description: Hiram Calvo We deal with deceptive text identification by using different kinds of features: a continuous semantic space model based on latent Dirichlet allocation topics (LDA), one-hot representation (OHR), syntactic information from syntactic n-grams (SN), and lexicon-based features using the linguistic inquiry and word count dictionary (LIWC). We will present experiments with several combinations of these features were tested to assess the best source(s) for deceptive text identification aiming to present a state of the art performance. We conducted our tests on three different available corpora: a corpus consisting of 800 reviews about hotels, a corpus consisting of 600 reviews about controversial topics, and a corpus consisting of 236 book reviews. Additionally, we present an analysis on which features lead to either deceptive or truthful texts, finding that certain words can play different roles (sometimes even opposing ones) depending on the task being evaluated. We will present results of experiments in one-domain setting by training and testing our models separately on each dataset (with fivefold cross-validation); in a mixed-domain setting by merging all datasets into one large corpus (again, with fivefold cross-validation), and finally, with cross-domain setting: using one dataset for testing and a concatenation of all other datasets for training.
Mardi 7 Mars
Heure: 11:30 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Valid quadratic inequalities for convex and some non-convex quadratic sets
Description: Julio César Góez In recent years, the generalization of Balas disjunctive cuts for mixed integer linear optimization problems to mixed integer non-linear optimization problems has received significant attention. Among these studies, mixed integer second order cone optimization (MISOCO) is a special case. For MISOCO one has the disjuncti ve conic cuts approach. That generalization introduced the concept of disjunctive conic cuts (DCCs) and disjunctive cylindrical cuts (DCyCs). Specifically, it showed that under some mild assumptions the intersection of those DCCs and DCyCs with a closed convex set, given as the intersection of a second order cone and an affine set, is the convex hull of the intersection of the same set with a linear disjunction. The key element in that analysis is the use of pencils of quadrics to find close forms for deriving the DCCs and DCyCs. In this talk we present an overview of the DCCs main results and we use the same approach to show the existence of valid conic inequalities for hyperboloids and non-convex quadratic cones when the disjunction is defined by parallel hyperplanes. Joint work with Miguel F. Anjos.
Jeudi 9 Mars
Heure: 10:30 - 11:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Hybride Modelling, Analysis and Quantitative Verification of Large Biological Regulatory Networks
Description: Louis Fippo Fitime Biological Regulatory Networks (BRNs) are usually used in systems biology for modelling,
understanding and controlling the dynamics of different biological functions (differentiation,
proliferation, proteins synthesis, apoptose) inside cells. Those networks are enhanced with
experimental data that are nowadays more available which give an idea on the dynamics of BRNs components.
Formal analysis of such models fails in front of the combinatorial explosion of generated behaviours
despite the fact that BRNs provide abstract representation of biological systems.

This thesis handles hybrid modelling, the simulation, the formal verification and control of Large
Biological Regulatory Networks. This modelling is done thanks to stochastic automata networks, thereafter
to Process Hitting by integrating time-series data.

Firstly, this thesis proposes a refining of the dynamics by estimation of stochastic and temporal (delay)
parameters from time-series data and integration of those parameters in automata networks models. This
integration allows the parametrisation of the transitions between the states of the system. Then,
a statistical analysis of the traces of the stochastic simulation is proposed to compare the dynamics
of simulations with the experimental data.

Secondly, this thesis develops static analysis by abstract interpretation in the automata networks
allowing efficient under- and over-approximation of quantitative (probability and delay) reachability properties.
This analysis enables to highlight the critical components to satisfy these properties.

Finally, taking advantage from the previous developed static analyses for the reachability properties in the
qualitative point of view, and from the power of logic programming (Answer Set Programming), this thesis addresses the domain
of control of system by proposing the identification of bifurcation transitions. Bifurcations are
transitions after which the system can no longer reach a state that was previously reachable.
Vendredi 10 Mars
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Retrofitting linear types
Description: Arnaud Spiwack Type systems based on linear logic and their friends have proved that they are both capable of expressing a wealth of interesting abstractions. Among these the ability to mix garbage-collected and explicitly managed data in the same language. This is of prime interest for distributed computations that need to reduce latency induced by GC pauses: a smaller GC heap is a happier GC heap.

I had always had the belief that to add linear types to a language was a rather intrusive procedure and that a language with linear types would basically be an entirely new language. The Rust language is a case in point: it has a linear-like type system, but it's a very different language from your run-of-the-mill functional language.

This turns out not to be the case: this talk presents a way to extend a functional programming language. We are targeting Haskell but there is little specific to Haskell in this presentation. I will focus mostly on the type system and how it can be generalised: among other things the type system extends to dependent types.
Mardi 14 Mars
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Géométrie combinatoire : densité d'hypergraphes et méthode probabiliste
Description: Xavier Goaoc Un hypergraphe à n sommets dont aucune projection sur k sommet n'est complète a au plus O(n^{k-1}) arêtes. Ce résultat, découvert simultanément par Sauer, Vapnick-Chervonenkis et Perles-Shelah au début des années 1970, est fondamental en apprentissage. En géométrie combinatoire et algorithmique, il permet souvent de contrôler la complexité (globale) d'une structure par sa "densité" locale. J'introduirai à ce mécanisme avant de présenter quelques extensions récentes, obtenues conjointement avec Boris Bukh (https://arxiv.org/abs/1701.06632), qui permettent un controle plus fin de la complexité. L'exposé ne supposera aucune connaissance préalable et un des ingrédients sera une construction probabiliste.
Jeudi 16 Mars
Heure: 15:30 - 16:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Preserving Partial Order Runs in Parametric Time Petri Nets
Description: Cesar Rodriguez Parameter synthesis for timed systems aims at deriving parameter
valuations satisfying a given property.
In this paper we target concurrent systems; it is well known that
concurrency is a source of state-space explosion, and partial order
techniques were defined to cope with this problem.
Here we use partial order semantics for parametric time Petri nets as a
way to significantly enhance the result of an existing synthesis
algorithm.
Given a reference parameter valuation, our approach synthesizes other
valuations preserving, up to interleaving,
the behavior of the reference parameter valuation.
We show the applicability of our approach using acyclic asynchronous circuits.

Join work with Thomas Chatain and Étienne André.
Vendredi 17 Mars
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Des preuves, oui, mais formelles !
Description: Micaela MAYERO Dans cet exposé, très informel, lui, je parlerai de l'évolution des outils de preuves formelles ces 20, voire ces 30, dernières années. Nous nous appuierons sur quelques exemples afin de montrer comment les formalisations contribuent à la fois au développement de ces outils via des avancés théoriques majeurs ainsi qu'aux domaines qui s'engagent peu à peu dans leur utilisation. Suite à une première partie accessible à tout public, nous parlerons de la logique sous-jacente à l'un des système connaissant le plus d'avancées et de changements: Coq. Nous aborderons les évolutions de la théorie des types avec (im)prédicativité, la logique classique avec le choix de la totalité et d'autres avancées, pour finir, si nous avons le temps, par quelques mots sur CoqHoTT et l'axiome d'univalence.
Jeudi 23 Mars
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: CARET Model Checking For Pushdown Systems
Description: Huu-Vu Nguyen CARET (A temporal logic of calls and returns) was introduced by Alur et al. This logic allows to write linear temporal logic formulas while taking into account matching of calls and returns. However, CARET model checking for Pushdown Systems (PDSs) was never considered in the literature. Previous works only dealt with the model checking problem for Recursive State Machine (RSMs). While RSMs are a good formalism to model sequential programs written in structured programming languages like C or Java, they become non suitable for modeling binary or assembly programs, since, in these programs, explicit push and pop of the stack can occur. Thus, it is very important to have a CARET model checking algorithm for PDSs. We tackle this problem in this paper. We also consider CARET model checking with regular valuations, where the set of configurations in which an atomic proposition holds is a regular language. We reduce these problems to the emptiness problem of Büchi Pushdown Systems. We implemented our technique in a tool, and we applied it to different case studies. Our results are encouraging. In particular, we were able to apply our tool to detect several malwares.

This is a joint work with Tayssir Touili.
Vendredi 24 Mars
Heure: 11:00 - 12:30
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Syntaxe transcendentale: seconde lecture.
Description: Christophe Fouqueré Suite de la première lecture: JY Girard, avec ses 3 articles sur la "syntaxe transcendentale", aborde la logique sous un angle à la fois philosophico-logique et sous un angle technique, pour aller au-delà de ce qui est fait jusqu'à présent: non seulement la logique linéaire propositionnelle mais encore le traitement de l'égalité donc du premier ordre. Modestement, je commencerai par présenter la partie technique, qui reprend et étend le modèle des réseaux de preuves, en présentant la représentation de MALL et des exponentielles.
Mardi 28 Mars
Heure: 14:00 - 17:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Phase Transition Threshold for Random Graphs and 2-SAT using Degree Constraints
Description: Sergey Dovgal We show that by restricting the degrees of the vertices of a graph to an arbitrary set ?, the threshold ?(?) of the phase transition for a random graph with n vertices and m = ?(?).n edges can be either accelerated (e.g.,?(?) approx 0.38 for ? = {0,1,4,5}) or postponed (e.g., ?(?) approx 0.95 for ?={1,2,50}) compared to a classical Erd?s?Rényi random graph where ?(N)=1/2. We investigate different graph statistics inside the critical window of transition (planarity, diameter, longest path...).We apply our results to a 2-SAT model with restricted literal degrees: the number of clauses that each literalis incident to belongs to the set ?. We prove a lower bound for the probability that a formula with n variables and m=2.?(?) n clauses is satisfiable. This probability is close to 1 for the subcritical regime m=2.?.n.(1-μ.n-1/3), μ to ∞ and improves/generalizes the lower bound of Bollobás, Borgs, Chayes, Kim, and Wilson.This shows how the phase transition threshold for 2-SAT moves if we change the degrees of the literals.Joint work with Vlady Ravelomanana.