Séminaire Performance et Généricité
À propos du séminaire
La modélisation orientée objet permet la classification des problèmes de calcul scientifique, et par conséquent, par la factorisation qu'elle rend possible, elle fournit un excellent support pour la fédération d'efforts de développement. Malheureusement les performances en pâtissent souvent. De nouveaux langages, de nouvelles techniques de programmation réconcilient performance et généricité, permettant la naissance de bibliothèques de nouvelle génération (Boost, Olena, Vaucanson, etc.).
L'objet de ce séminaire est la diffusion du savoir et des compétences sur la modélisation de bibliothèques métiers génériques et performantes.
Mots clés: Calcul Scientifique, Distribution, Génie Logiciel, Généricité, Grille, Langages, Multi-cœur, Paradigmes de Programmation, Parallélisme, Recherche reproductible.
Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems
Daniel Stan, Technische Universität Kaiserslautern
We present a framework for modelling and verifying epistemic properties over parameterized multi-agent systems that communicate by truthful public announcements. In this framework, the number of agents or the amount of certain resources are parameterized (i.e. not known a priori), and the corresponding verification problem asks whether a given epistemic property is true regardless of the instantiation of the parameters. As in other regular model checking (RMC) techniques, a finite-state automaton is used to specify a parameterized family of systems.
Parameterized systems might also require an arbitrary number of announcements, leading to the introduction of the so-called iterated public announcement. Although model checking becomes undecidable because of this operator, we provide a semi-decision procedure based on Angluin's L*-algorithm for learning finite automata. Moreover, the procedure is guaranteed to terminate when some regularity properties are met. We illustrate the approach on the Muddy Children puzzle, and we further discuss dynamic protocol encodings through the Dining Cryptographer example.
Initial publication at AAMAS21, joint work with Anthony Lin and Felix Thomas
Since October 2019, Daniel Stan is a PostDoc in the Automated Reasoning group.
He was previously a PhD student (2013-2017) at LSV, ENS Paris Saclay under the
supervision of Patricia Bouyer and Nicolas Markey, then a PostDoc in the
Dependable Systems and Software chair of Saarbrücken. His research interests
include formal methods and model checking techniques with a particular focus on
Regular Model Checking and Automatic Structures, Parameterized Systems,
Stochastic Systems and Games. In particular, his current work put an emphasis on
exact learning algorithms with applications to model checking.
Scaling Optimal Transport for High Dimensional Learning
Gabriel Peyré, CNRS and Ecole Normale Supérieure
Optimal transport (OT) has recently gained a lot of interest in machine learning. It is a natural tool to compare in a geometrically faithful way probability distributions. It finds applications in both supervised learning (using geometric loss functions) and unsupervised learning (to perform generative model fitting). OT is however plagued by the curse of dimensionality, since it might require a number of samples which grows exponentially with the dimension. In this talk, I will review entropic regularization methods which define geometric loss functions approximating OT with a better sample complexity.
Gabriel Peyré is a CNRS senior researcher and professor at Ecole Normale Supérieure, Paris. He works at the interface between applied mathematics, imaging and machine learning. He obtained 2 ERC grants (Starting in 2010 and Consolidator in 2017), the Blaise Pascal prize from the French academy of sciences in 2017, the Magenes Prize from the Italian Mathematical Union in 2019 and the silver medal from CNRS in 2021. He is invited speaker at the European Congress for Mathematics in 2020. He is the deputy director of the Prairie Institute for artificial intelligence, the director of the ENS center for data science and the former director of the GdR CNRS MIA. He is the head of the ELLIS (European Lab for Learning & Intelligent Systems) Paris Unit. He is engaged in reproducible research and code education.
https://optimaltransport.github.io/, http://www.numerical-tours.com/, https://ellis-paris.github.io/
An Introduction to Topological Data Analysis with the Topology ToolKit
Julien Tierny, Sorbonne Université
Topological Data Analysis (TDA) is a recent area of computer science that focuses on discovering intrinsic structures hidden in data. Based on solid mathematical tools such as Morse theory and Persistent Homology, TDA enables the robust extraction of the main features of a data set into stable, concise, and multi-scale descriptors that facilitate data analysis and visualization. In this talk, I will give an intuitive overview of the main tools used in TDA (persistence diagrams, Reeb graphs, Morse-Smale complexes, etc.) with applications to concrete use cases in computational fluid dynamics, medical imaging, quantum chemistry, and climate modeling. This talk will be illustrated with results produced with the "Topology ToolKit" (TTK), an open-source library (BSD license) that we develop with collaborators to showcase our research. Tutorials for re-producing these experiments are available on the TTK website.
Julien Tierny received his Ph.D. degree in Computer Science from the University of Lille in 2008 and
the Habilitation degree (HDR) from Sorbonne University in 2016. Currently a CNRS permanent
research scientist affiliated with Sorbonne University, his research expertise lies in topological methods
for data analysis and visualization. Author on the topic and award winner for his research, he regularly
serves as an international program committee member for the top venues in data visualization (IEEE VIS,
EuroVis, etc.) and is an associate editor for IEEE Transactions on Visualization and Computer Graphics.
Julien Tierny is also founder and lead developer of the Topology ToolKit (TTK), an open source library for
topological data analysis.
- Adresse et plan
- Recevoir les annonces par email :