Interdisciplinary seminar

 9:00

 IRMA Conference Room and online https://bbb.unistra.fr/b/hum-51d-suf-mzq

Abstract: Formal Verification enables one to prove that a program does not contain any bug. In this talk, I will present state-of-the-art techniques for formally verifying the implementation of a nontrivial algorithm or data structure. First, I will explain how to formulate as a mathematical theorem a statement of the form: "this program behaves as intended". Second, I will explain how to leverage an "interactive proof assistant", a tool for developing machine-checked mathematical proofs, for reasoning about the behavior of the source code of the program. Finally, I will give a survey of complex programs that have been formally verified in the past decade, assessing the progress made since the pioneering work by Hoare-Floyd-Dijkstra in the late 60's.

About the speaker: Arthur Charguéraud is an Inria researcher, member of the ICube lab since 2016. He completed his PhD in 2010 at Inria Paris-Rocquencourt, then spent 18 months as a post-doc at the Max Plank Institute for Software Systems in Kaiserslautern. He was recruited at Inria Saclay in 2012, then moved to Strasbourg in 2016. His research is focused on program verification and program optimization.

 9:00

 IRMA Conference room and online https://bbb.unistra.fr/b/hum-51d-suf-mzq

Abstract: Kinetically constrained models are a class of mathematical models introduced by physicists to describe the behavior of glass. Each element of Z^2 is in state 0 or 1, and can change state at random times, but only when a constraint of the form "there are enough zeros around the element" is satisfied. There is an infinite number of possible constraints, and the properties of a model sharply depend on the constraint chosen. Therefore a very important question is that of universality: can this infinite number of models be divided into a finite number of classes depending on their behavior ? The answer is yes, and in this talk we will explain how.

About the speaker: Laure Marêché has been an assistant professor in mathematics at Université de Strasbourg and a researcher at IRMA since 2020. She obtained her PhD in 2019 at Université Paris Diderot. After that, she did a post-doc at École Polytechnique Fédérale de Lausanne. She works in the field of probability, more precisely in statistical mechanics.

Abstract: Since their introduction into cosmology, Minkowski functionals have been applied to various problems regarding the morphology of the large-scale structure of the Universe, but also the smaller-scale objects such as galaxy clusters and dark matter halos. Minkowski functionals represent a complete family of morphological measures describing the content, shape and connectivity of the underlying density field. In this talk, I will give a short comprehensible introduction into integral geometry alongside the interpretation of the Minkowski functionals in 3 dimensional Euclidean space. I will then show some applications of all four Minkowski functionals in different configurations, namely the distribution of observed galaxies in our Universe, and the distribution of matter in simulations with different initial conditions or ingredients. These morphological descriptors incorporate correlations of arbitrary order and therefore provide a complementary look at large-scale structure that could potentially reveal the presence of (primordial) non-Gaussianities, but also provide constraints on poorly known baryonic processes such as stellar or black hole feedback.

About the speaker:Katarina Kraljic is a CNRS researcher in the GALHECOS team at Strasbourg Observatory since 2022. After finishing her PhD at CEA-Saclay in 2014, she moved to Marseille for a post-doctoral appointment. She then spent 3 years as a postdoctoral fellow at the Royal Observatory in Edinburgh, before returning to Marseille in 2020 and then Strasbourg in 2022. Her research focuses on the formation and evolution of galaxies, the large-scale structure of the Universe, the internal structure of galaxies and their interstellar medium, with the aim to better understand the complete cosmic baryon cycle, both from a theoretical and observational perspective.

Presentation content: Click here to see the presentation - Click here to download the content

Abstract: L’Eau, ressource indispensable à la vie sur Terre, est de nos jours, sujette à de multiples pressions naturelles et anthropiques qui modifient voire altèrent ses états. Répondre en qualité et quantité aux besoins en eau de l’humanité sans nuire à la pérennité de la ressource et des écosystèmes nécessite une gestion intégrée à une échelle spatiale judicieusement déterminée. Face à l’urgence climatique inspirée des recommandations du GIEC (2013) et considérant l’accélération des transformations urbaines, les collectivités territoriales mènent de front des stratégies d’adaptation et d’atténuation. Ces stratégies intègrent l’implémentation des Solutions Fondées sur la Nature (SFN) qui sont des dispositifs relevant de l’ingénierie écologique. La compréhension de la trajectoire de ces SFN, des processus en jeu, de leurs fonctions écologiques et des services qu’elles offrent sont au cœur des recherches que je présenterais. Après des généralités, je ferais un focus sur différentes applications pour lesquels des modèles mathématiques ont permis de clarifier la compréhension des processus clés au sein des écosystèmes complexes.

About the speaker:Professeur en sciences de l’eau et génie de l’environnement à l’ENGEES, A. Wanko est co-responsable de l’équipe Mécanique des Fluides d’ICube et animateur de la thématique « Eau & durabilité » de la Zone Atelier Environnemental Urbaine (Zaeu), labellisée par l'Institut écologie et environnement (INEE) du Centre national de la recherche scientifique (CNRS). Thèmes de recherche : transferts de matière en milieux poreux, modélisation du couplage hydrodynamique et transferts réactifs en ingénierie écologique, phytoremediation des eaux, phytoremediation des sols, hydrologie urbaine durable.

Presentation content: Click here to see the presentation - Click here to download the content

Abstract: In this talk, I will present a (non-exhaustive) review of the state-of-the-art of our current standard cosmological model. I will show how we manipulate stochastic (quasi-)Gaussian random fields living on a curved spacetime and how we evolve them through cosmic history. I will then show that for the final stages of the cosmic evolution, when the evolution becomes too non-linear, a numerical approach prevails. I will then present you how some of the (high performance computing) simulations that we are are currently developing at the observatory, with non-Gaussian initial conditions, could (perhaps) be a game changer for the field of galaxy formation.

About the speaker:Clément Stahl is a postdoc in the GALHECOS team at Strasbourg Observatory since 2021. He obtained his PhD at the University of La Sapienza (Rome) in 2017. Before, he was a postdoctoral fellow in Valparaiso (Chile) and at the Laboratoire Astroparticules & Cosmologie (APC, Paris). His research interests include inflation, large scale structure, dark matter and dark energy both from a theoretical and numerical point of view.

Presentation content: Click here to download

 

Abstract:  I will start with the well-known subject of addition chains, which describe the best possible ways of raising an element to a certain power, in any group (or even monoid). These are used by all computer algebra packages, when you request them to compute a high power of a large matrix, for example. Then I will say a word about the more general problem of computing in other groups, facing questions such as: when A and B are matrices, how many multiplications do you need to compute ABABABABABABABABABABABABABABABAB ? (Answer: just 4.) Very little is known in general. Finally, I will explain how similar ideas can be used to describe the "assembly index" of any object, as was recently exploited by chemists. It turns out that the assembly index of molecules can be measured experimentally rather than computed, and this opens up the possibility of detecting the presence of life on other planets. Accordingly, the talk will end with pictures of aliens.

About the speaker:Pierre Guillot is a reader in mathematics at the university of Strasbourg, and a researcher at IRMA. He obtained his PhD at the university of Cambridge (UK) in 2004, was a postdoctoral fellow in Lille and Nice before being appointed lecturer at Strasbourg. His research interests include group cohomology, Galois theory, algebraic topology and computational algebra.

Presentation content : Click here to download

Abstract: Mathematical morphology is a discipline that was developed in 1964 by Georges Matheron and Jean Serra, with the objective of characterizing and quantifying objects and structures in images by the means of sets, and more generally complete lattices. Since then, mathematical morphology can be seen as a convenient toolkit providing many operators to solve practical image processing problems. In this context, connected operators are a class of operators having the property to perserve image contours: a contour is either retained or removed, but cannot be moved.

In this talk, I will present hierarchical data structures enabling to design and compute efficiently connected operators. In particular, the max-tree, or component-tree, is a structure that is build from the level-sets of an image by storing in its nodes the connected components of the threshold sets and their inclusion relationship in its edges. On this basis, I will present an extension of this concept to color and multivalued images that we have called "component-graph". I will also present some recent results in the field of semantic segmentation involving max-trees, deep-learning and topological constraints. These concepts will be illustrated on biomedical applications.

About the speaker:Benoît Naegel is a professor in Computer Science. He obtained his PhD in the field of mathematical morphology applied to medical image analysis in 2004. From 2005 to 2007 he was a post-doctoral fellow at the University of Applied Sciences of Western Switzerland in Geneva where he worked on several biomedical projects in collaboration with the Hospital of Geneva. From 2007 to 2011 he was with the LORIA laboratory, Nancy, in the QGAR team dedicated to document processing. He is a member of ICube laboratory since 2011 where he conducts research in mathematical morphology and deep learning applied to biomedical imaging.

Abstract: The symplectic non-squeezing theorem, discovered by Gromov in 1985, has been the first result showing a fundamental difference between symplectic transformations, which form the mathematical framework for classical mechanics, and volume preserving ones. A similar but more subtle phenomenon in contact topology, the odd dimensional cousin of symplectic topology, has been found by Eliashberg, Kim and Polterovich in 2006, and refined by Fraser in 2016 and Chiu in 2017: in this case non-squeezing depends on the size of the domains, and only appears above a certain quantum scale. In my talk I will describe these fundamental results of symplectic and contact topology, briefly mentioning their relation to classical and quantum mechanics.

About the speaker: Sheila (Margherita) Sandon is a CNRS junior researcher at IRMA. She graduated from IST Lisbon with a Ph.D. degree in 2009. After a postdoctoral stay at the University of Nantes and a 2 year visit at the UMI-CNRS of the University of Montreal, she joined IRMA in 2014. She works in symplectic and contact topology.

Presentation content:Click here to see the presentation

Abstract: A large observational effort is currently underway to better probe and understand the first billion years of the Universe, an epoch from which we know very little, because of the enormous distances involved, making its observation very difficult. The new observational means involve giant radio telescopes on the ground, as well as new facilities in space (e.g., the JWST), focusing on the intergalactic medium and forming galaxies, respectively, to give us a new, complementary view of the early universe. To prepare and interpret these upcoming data, numerical simulations of the early Universe are required, involving a wide range of physics and requiring a variety of numerical approaches. I will showcase the recent works of our group in this field, including the largest simulation of the Epoch of Reionization ever made, Cosmic Dawn III (https://coda-simulation.github.io/), performed on Summit at Oak Ridge Leadership Computing Facility, the challenges it presented, and some of the challenges ahead.

About the speaker: Pierre Ocvirk is Astronome Adjoint at Observatoire de Strasbourg and member of the CDS (Centre de Données de Strasbourg). His research focuses on the modelling of the epoch of reionization using giant simulations, and galaxy formation with an emphasis on hydro-radiative processes.

Presentation content: Click here to see the presentation

Abstract: The first part will consist of a short introduction to the field of computer verified proofs. Why verify proofs with a computer? what can be verified? what are the challenges? In a second part, I will give an overview of our formalizations concerning the foundations of geometry based on the axiom systems of Hilbert, Tarski and Euclid. In particular, I will present a joint work with Michael Beeson and Freek Wiedijk which consisted in mechanically verifying the proofs of the first book of Euclid's Elements while trying to stay as close as possible to the original proofs. I will discuss the classification of 34 versions of the axioms of parallels (joint work with Pierre Boutry). We will finish by presenting a syntactic proof of the independence of the axiom of parallels (joint work with Michael Beeson and Pierre Boutry).

About the speaker: Julien Narboux is Maître de Conférences at the Université de Strasbourg, and pursues his research at ICube (IGG team). His research interests include formal proofs and formalisation of foundations of geometry and applications. He is especially interested in automated reasoning (in particular in geometry) and using proof assistants for teaching.

Presentation content: Click here to see the presentation

Abstract: We will start the talk by recalling classical facts from Morse theory. In other words we will discuss the following classical question: what do the critical points of a function on a manifold tell us about the topology of the manifold? After that we will discuss the following question. Given a manifold M and a smooth map f from M to the circle, can we deform f to a map which has no critical points? Or a minimal number of critical points ?

About the speaker: Pierre Py is a CNRS junior researcher at IRMA. He graduated from ENS Lyon with a Ph.D. degree in 2008. After a postdoctoral stay at the University of Chicago, he joined IRMA as a CNRS researcher in 2011. His research interests evolved over time from the study of symplectic diffeomorphism groups towards Kähler geometry and its interactions with topology and geometric group theory.

Abstract: I will present the state of the art on theoretical/numerical modelling of the magnetic reconnection process that is believed to be the central mechanism at work to explain magnetic eruptions in many astrophysical plasmas. In particular, I will highlight the main limitations when using standard numerical schemes to integrate the relevant set of partial differential equations in the magnetohydrodynamic framework. Finally, I will present hope for future numerical strategy based on machine/deep learning trough physics-informed neural networks.

About the speaker: Hubert Baty is Maître de Conférences at the University of Strasbourg, and pursues his research at the Observatoire astronomique de Strasbourg. His research focuses on instabilities and magnetic reconnection in magnetically-dominated plasmas with applications to solar/stellar corona and astrophysical jets.

Abstract: Numerical simulations inevitably requires the use of modern visualization methods at different stages to analyze datasets, extract information from them, to guide phenomenon modeling, to validate or invalidate models or as a tool for evaluating experimental results. The access to increasingly powerful computing machines enables scientists to simulate ever larger and more complex phenomena. Large-scale simulations generally output time-varying multivariate volumetric data, modeled by volume meshes of increasingly complex size, topology, geometry, composition, ... Direct volume rendering (DVR) is a well known method for visualizing volume data and its implementation on graphics processors (GPU), based on volume ray-casting algorithm, offers good rendering quality combined to good performance. However, such an implementation on simulated data presenting above-mentioned characteristics is a difficult problem that remains open. A key challenge of research is to make visualization techniques follow up with this drastically increasing complexity.

After an introduction to volume rendering on GPU and its adaptation to large datasets, I will address the challenges of in-situ visualization of large and complex unstructured meshes from numerical simulation through the presentation of the ANR LUM-Vis project.

About the speaker: Jonathan Sarton is an associate professor at the University of Strasbourg in the computer science department, and the ICube Laboratory in the Computer Graphics and Geometry team (IGG).  His research focuses on high performance scientific visualization, volume rendering on GPU, parallel rendering, and in-situ visualization in HPC environment. He is the scientific leader of the LUM-Vis ANR project.

Abstract: Strongly-correlated quantum systems are often extremely fragile and notoriously hard to control, which poses challenges for possible technological applications. That is why a certain subclass of quantum states, the so-called topological phases of matter, recently attracted much attention. These are characterised by a certain degree of stability and robustness under perturbations, rooted in their special mathematical properties. Apriori, it is not always clear whether a given quantum state of matter is topological or not. We propose a mathematical criterion, which we call “the geometric test", to tell whether a state of matter is in a topological phase. We then apply our test to strongly-interacting states of matter in Quantum Hall effect, observed in certain 2d materials (Gallium-arsenide, graphene, ...) at low temperatures and in strong magnetic fields. I will explain the idea of the test (which works pretty well) and the results, based on recent work with Dimitri Zvonkine (CNRS, Versailles Mathematics Laboratory, Paris-Saclay University, France).

About the speaker:  Semyon Klevtsov obtained his PhD in 2009 at Rutgers University (USA), working on mathematical aspects of string theory. After a post-doctoral stays in Brussels and Cologne, he joined the Institute for Advanced Mathematical Research (IRMA) at the University of Strasbourg, as professor of mathematical physics. His most recent research is focused on mathematical aspects of the strongly correlated electron systems in condensed matter physics.

Abstract

: The MLIR compiler framework is a novel compiler infrastructure that eases the process of developing new interacting compiler passes, built on top of the LLVM compiler. According to mlir.llvm.org, it especially "significantly reduces the cost of building domain specific compilers". I will shortly introduce MLIR and explain how to generate optimized compiled code using this framework.

Then, I will present our experience in the MICROCARD European project (https://microcard.eu/), in collaboration with INRIA Bordeaux and KIT among other partners. Our aim is to write software to simulate cardiac electrophysiology using whole-heart models with sub-cellular resolution, on future exascale supercomputers. It builds on the existing open source openCARP project (opencarp.org), a cardiac electrophysiology simulator for in-silico experiments. OpenCARP includes a solver and the ionic model component describing ionic transmembrane currents, as ordinary differential equations (ODEs). They are provided using a DSL (domain specific language) for ODEs named easyML. The easyML input is analyzed and transformed into code by a python parser, which we modified to plug it to MLIR and generate OpenMP and vectorized efficient code. MLIR can also be used to generate GPU code, and we plan to experiment with this in the near future.

About the speaker: Vincent Loechner is assistant professor at University of Strasbourg in the computer science department, and the ICube Laboratory in the parallelism team (ICPS). He is also part of the INRIA CAMUS team. He is in charge of the compilation and code optimization work-package of the MICROCARD European project.

Abstract: The physical processes driving galaxy formation and evolution span a vast range of scales, from the large scale structures of the universe to the turbulent interstellar medium and the interactions between light and matter. In this talk, I will present some of the empirical scaling relations that guide our understanding of these complex physical processes, focussing notably on the fate of gas within galaxies, star formation, and the relation between galaxies and their surrounding dark matter haloes.

About the speaker: Jonathan Freundlich did his Ph.D. between 2012 and 2015 at the Paris Observatory, probing star formation across cosmic time and modelling the influence of baryons on dark matter haloes. He was afterwards a postdoc at the Hebrew University of Jerusalem, where he gained experience in analysing cosmological simulations. He became Maître de Conférences at the Strasbourg Observatory in 2021, within the Galaxies, High Energy, Cosmology, Compact Objects & Stars (GALHECOS) research group.

Abstract: In this talk, we want to introduce different examples or problems of interaction between deep learning, geometry, PDEs and numerical methods. We will start by illustrating the ability of deep learning to deal with physical problems starting from a classical problem in fluid mechanics: the closure. In a second step, we will introduce recent works mixing learning and differential geometry which allow to tackle unstructured data. We will illustrate this with simple examples from PDEs. Finally, we will show how ideas from analytical mechanics (and symplectic geometry) can interact with machine learning and numerical simulations of PDEs.

About the speaker: Emmanuel Franck did his Ph.D. thesis from 2009 to 2012 at the CEA on the numerical approximation of the radiative transfer equation. After that he did a 2 year post-doc at the Max Planck Institute for Plasma Physics in Munich on numerical methods for MHD in nuclear fusion. He is an INRIA young researcher since 2014 and his work focuses on the numerical approximation of PDEs in fluid mechanics and plasma physics. He is a member of the Modelling and Control (MOCO) research group at IRMA, Strasbourg.