Journée MDSC 2019

Programme de la Journée MDSC 25 Juin 2019

  • 09h30 - 10h00

Accueil Café (Salle 121, Bâtiment Forum, Sophia Antipolis)

  • 10h00 - 11h00

Randomness spaces and cellular automata dynamics

(Enrico Formenti)
Randomness spaces were introduced by Hertling and Weihrauch in 1998 as a setting for defining randomness in general topological spaces. Afterwards, Calude et al. translated the technique to full shift spaces and analyzed the randomness behavior of cellular automata. Another approach to the study of randomness in dynamical systems, an in particular of cellular automata has been proposed by Cervelle, Durand and Formenti in 2001. In this talk we compare both approaches and conclude with a series of open questions.

(Slides)

  • 11h00 - 11h15

Pause

  • 11h15 - 11h50

Key exchange protocols over voice channels and verification using Tamarin Prover

(Piotr Krasnowski)
Secure communications over real-time voice channels require a prior exchange of cryptographic keys. However, due to the distortive nature of real-time voice channels, classical key exchange protocols are not suitable. The goal of this talk is to introduce to the problem of key exchange protocols over voice channels. A toy key exchange protocol will be presented along with the verification by Tamarin – an automated security protocol verification tool developed at ETH Zurich.

(Slides)

  • 11h50 - 12h25

SAT solvers: how and why do they work?

(Valentin Montmirail)
Within two decades, the use of SAT related technology moved from a confidential interest among specialists to a popular tool for solving some discrete combinatorial problems. Improvements in the practical resolution of SAT is driven by applications: Bounded Model Checking in Electronic Design Automation has been a major component for the success of SAT engines for solving "real" combinatorial problems at the end of the 90s, Bioinformatic and Software engineering are currently two areas where SAT engines receive a lot of interest. In this talk, we will focus on modern SAT solvers tailored to solve "real" combinatorial problems, and on why they are so efficient at this task. This talk will introduce the generic SAT engine architecture used in any CDCL SAT solver and we will discuss some implementation details to make them work in practice.

  • 12h30 - 14h30

Pause

  • 14h30 - 15h00

SAT et DDS: une étude expérimentale.

(Sara Riva)
Boolean automata networks, genetic regulation networks, and metabolic networks are just a few examples of biological modeling by discrete dynamical systems (DDS). A major issue in modeling is the verification of the model against the experimental data or inducing the model under uncertainties in the data. Equipping finite discrete dynamical systems with an algebraic structure of semiring provides a suitable context for hypothesis verification on the dynamics of DDS. Indeed, hypothesis on the systems can be translated into polynomial equations over DDS. Solutions to these equations provide the validation to the initial hypothesis. Unfortunately, finding solutions to general equations over DDS is undecidable. However, many tractable cases have been highlighted. In this article, we want to push the envelop further by proposing a practical approach for such cases. We demonstrate that for many tractable equations all goes down to a "simpler'' equation. However for us, the problem is not to decide if the simple equation has a solution, but to enumerate all the solutions in order to provide an insight on the set of solutions of the original, undecidable, equations. We evaluate experimentally our approach and show that it has good scalability property, but this approach can be improved with dynamic programming or with the problem modeling in SAT, this achieves the best performance.

  • 15h00 - 15h30

Combinaison des approches par partitionnement et par portfolio en programmation par contraintes.

(Samvel Dersarkissian)
La programmation par contraintes est une technique élégante permettant de résoudre des problèmes combinatoires. Cependant la résolution de problèmes complexes peut être longue. Une façon de rendre ces calculs plus rapides est la parallélisation qui permet de tirer pleinement profit des processeurs multicœurs modernes. La méthode Embarrassingly Parallel Search (EPS) est basée sur la décomposition d’un problème en un très grand nombre de sous-problèmes disjoints qui sont ensuite résolus en parallèle par des unités de calcul avec très peu, voire aucune communication. C’est une méthode générique mais son implémentation ne l’est pas. Actuellement il y a une implémentation spécifique pour chaque plateforme (machine multi-cœurs, réseau de machines, centre de calculs, cloud, etc.). Nous cherchons à définir une architecture qui permette d’avoir une unique implémentation. En particulier nous souhaitons obtenir une architecture générale, indépendante des spécificités de bas niveau, et permettant de mettre en œuvre différents paradigmes de programmation (concurrence, parallélisme, distribution).

  • 16h00 - 18h00

Réunion d'équipe