Author: "Inria Nancy - Grand Est" - Searchworks@Jio Institute Digital Library Search Results

Your search keyword '"Inria Nancy - Grand Est"' showing total 7,064 results

Start Over Author "Inria Nancy - Grand Est"

7,064 results on '"Inria Nancy - Grand Est"'

1. On a class of switched linear systems

Author: CORIDA (INRIA Nancy - Grand Est / IECN / LMAM) ; CNRS - CNRS - INRIA - Université de Lorraine, Institut Elie Cartan Nancy (IECN) ; CNRS - INRIA - Université Henri Poincaré - Nancy I - Université Nancy II - Institut National Polytechnique de Lorraine (INPL), Centre de recherche en automatique de Nancy (CRAN) ; CNRS - Université Henri Poincaré - Nancy I - Institut National Polytechnique de Lorraine (INPL), CPER MISN: AOC action SC2, European Project : 232501, SME, FP7-SME-2008-1, HYCON(2009), Serres, Ulysse, Vivalda, Jean-Claude, Riedinger, Pierre, CORIDA (INRIA Nancy - Grand Est / IECN / LMAM) ; CNRS - CNRS - INRIA - Université de Lorraine, Institut Elie Cartan Nancy (IECN) ; CNRS - INRIA - Université Henri Poincaré - Nancy I - Université Nancy II - Institut National Polytechnique de Lorraine (INPL), Centre de recherche en automatique de Nancy (CRAN) ; CNRS - Université Henri Poincaré - Nancy I - Institut National Polytechnique de Lorraine (INPL), CPER MISN: AOC action SC2, European Project : 232501, SME, FP7-SME-2008-1, HYCON(2009), Serres, Ulysse, Vivalda, Jean-Claude, and Riedinger, Pierre
Abstract: International audience, This paper investigates sucient conditions for the convergence to zero of the trajectories of linear switched systems. We provide a collection of results that use weak dwell-time, dwell-time, strong dwell-time, permanent and persistent activation hypothesis. The obtained results are shown to be tight by counterexample. Finally, we apply our result to the three-cell converter.

2. An LQ sub-optimal stabilizing feedback law for switched linear systems

Author: Centre de Recherche en Automatique de Nancy (CRAN) ; Université de Lorraine - CNRS, CORIDA (INRIA Nancy - Grand Est / IECN / LMAM) ; CNRS - CNRS - INRIA - Université de Lorraine, Équations aux dérivées partielles ; Institut Élie Cartan de Lorraine (IECL) ; Université de Lorraine - CNRS - Université de Lorraine - CNRS, CORIDA, European Project : 257462, ICT, FP7-ICT-2009-5, HYCON2(2010), Riedinger, Pierre, Vivalda, Jean-Claude, Centre de Recherche en Automatique de Nancy (CRAN) ; Université de Lorraine - CNRS, CORIDA (INRIA Nancy - Grand Est / IECN / LMAM) ; CNRS - CNRS - INRIA - Université de Lorraine, Équations aux dérivées partielles ; Institut Élie Cartan de Lorraine (IECL) ; Université de Lorraine - CNRS - Université de Lorraine - CNRS, CORIDA, European Project : 257462, ICT, FP7-ICT-2009-5, HYCON2(2010), Riedinger, Pierre, and Vivalda, Jean-Claude
Abstract: International audience, The aim of this paper is the design of a stabilizing feedback law for contin- uous time linear switched system based on the optimization of a quadratic criterion. The main result provides a control Lyapunov function and a feed- back switching law leading to sub optimal solutions. As the Lyapunov func- tion defines a tight upper bound on the value function of the optimization problem, the sub optimality is guaranteed. Practically, the switching law is easy to apply and the design procedure is effective if there exists at least a controllable convex combination of the subsystems.

3. A Very Easy High-Order Well-Balanced Reconstruction for Hyperbolic Systems with Source Terms

Author: Christophe Berthon, Solène Bulteau, Françoise Foucher, Meissa M'Baye, Victor Michel-Dansac, Laboratoire de Mathématiques Jean Leray (LMJL), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-Centre National de la Recherche Scientifique (CNRS), Maison de la Simulation (MDLS), Université de Versailles Saint-Quentin-en-Yvelines (UVSQ)-Institut National de Recherche en Informatique et en Automatique (Inria)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS), École Centrale de Nantes (ECN), Laboratoire de Mathématique de la Décision et d'Analyse Numérique (L.M.D.A.N), Université Cheikh Anta Diop [Dakar, Sénégal] (UCAD), TOkamaks and NUmerical Simulations (TONUS), Institut de Recherche Mathématique Avancée (IRMA), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Christophe Berthon acknowledges the support of ANR MUFFIN ANR-19-CE46-0004., ANR-19-CE46-0004,MUFFIN,Multiéchelle et Trefftz pour le transport numérique(2019), ANR-11-LABX-0020,LEBESGUE,Centre de Mathématiques Henri Lebesgue : fondements, interactions, applications et Formation(2011), Centre National de la Recherche Scientifique (CNRS)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN), and Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Inria Nancy - Grand Est
Subjects: MSC 2010: 65M08, 65M12, Computational Mathematics, Hyperbolic conservation laws, Applied Mathematics, Well-balanced schemes, Balance laws, [MATH.MATH-AP]Mathematics [math]/Analysis of PDEs [math.AP], High-order reconstruction techniques, [MATH.MATH-NA]Mathematics [math]/Numerical Analysis [math.NA]
Abstract: International audience; When adopting high-order finite-volume schemes based on MUSCL reconstruction techniques to approximate the weak solutions of hyperbolic systems with source terms, the preservation of the steady states turns out to be very challenging. Indeed, the designed reconstruction must preserve the steady states under consideration in order to get the required well-balancedness property. A priori, to capture such a steady state, one needs to solve some strongly nonlinear equations. Here, in order to preserve the required well-balancedness property to be satisfied by finite volume methods, we design a very easy correction. This correction can be applied to any scheme of order greater than or equal to 2, such as a MUSCL-type scheme, and ensures that this scheme exactly preserves the steady solutions. The main discrepancy with usual techniques lies in never having to invert the nonlinear function governing the steady solutions. Moreover, for under-determined steady solutions, several nonlinear functions must be considered simultaneously. Since the derived correction only considers the evaluation of the governing nonlinear functions, we are able to deal with under-determined stationary systems. Several numerical experiments illustrate the relevance of the proposed well-balanced correction.
Published: 2022
Full Text: View/download PDF

4. A robust and efficient solver based on kinetic schemes for Magnetohydrodynamics (MHD) equations

Author: Hubert Baty, Florence Drui, Philippe Helluy, Emmanuel Franck, Christian Klingenberg, Lukas Thanhäuser, Observatoire astronomique de Strasbourg (ObAS), Université de Strasbourg (UNISTRA)-Institut national des sciences de l'Univers (INSU - CNRS)-Centre National de la Recherche Scientifique (CNRS), Commissariat à l'énergie atomique et aux énergies alternatives (CEA), TOkamaks and NUmerical Simulations (TONUS), Institut de Recherche Mathématique Avancée (IRMA), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), University of Würzburg, Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Institut national des sciences de l'Univers (INSU - CNRS), Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Inria Nancy - Grand Est, and Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)
Subjects: Computational Mathematics, Applied Mathematics, [MATH.MATH-AP]Mathematics [math]/Analysis of PDEs [math.AP], [MATH.MATH-NA]Mathematics [math]/Numerical Analysis [math.NA]
Abstract: This paper is devoted to the simulation of Magnetohydrohynamics (MHD) flows with complex structures. This kind of flow present instabilities that generate shock waves. We propose a robust and accurate numerical method based on the Lattice Boltzmann methodology. We explain how to adjust the numerical viscosity in order to obtain stable and accurate results in smooth or discontinuous parts of the flow, and reduced divergence errors. This method can handle shock waves and can be made second order in smooth regions. It is also very well adapted to computing with Graphics Processing Unit (GPU). We also give results for a tilt instability test case on very fine meshes.
Published: 2023
Full Text: View/download PDF

5. Polite Combination of Algebraic Datatypes

Author: Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark Barrett, Computer Science Department [Stanford], Stanford University, Department of Computer Science at Bar Ilan University, Bar-Ilan University [Israël], Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Massachusetts Institute of Technology, Computer Science and Artificial Intelligence Laboratory, Université de Liège, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), and Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est
Subjects: Algebraic datatypes, Satisfiability Modulo Theories, Polite combination, Computational Theory and Mathematics, Artificial Intelligence, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Automated reasoning, Theory combination, Software
Abstract: International audience; Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing how it can be combined with other arbitrary disjoint theories using polite combination. The combination method uses a new, simple, and natural notion of additivity that enables deducing strong politeness from (weak) politeness.
Published: 2022
Full Text: View/download PDF

6. Geometric and probabilistic results for the observability of the wave equation

Author: Emmanuel Humbert, Yannick Privat, Emmanuel Trélat, Institut Denis Poisson (IDP), Centre National de la Recherche Scientifique (CNRS)-Université de Tours-Université d'Orléans (UO), Institut de Recherche Mathématique Avancée (IRMA), Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA), TOkamaks and NUmerical Simulations (TONUS), Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire Jacques-Louis Lions (LJLL (UMR_7598)), Université Paris Diderot - Paris 7 (UPD7)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Control And GEometry (CaGE ), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Jacques-Louis Lions (LJLL (UMR_7598)), Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP), Centre National de la Recherche Scientifique (CNRS)-Université de Tours (UT)-Université d'Orléans (UO), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Université d'Orléans (UO)-Université de Tours (UT)-Centre National de la Recherche Scientifique (CNRS), Institut Universitaire de France (IUF), Ministère de l'Education nationale, de l’Enseignement supérieur et de la Recherche (M.E.N.E.S.R.), Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Université d'Orléans (UO)-Université de Tours-Centre National de la Recherche Scientifique (CNRS), and Université Paris Diderot - Paris 7 (UPD7)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)
Subjects: [MATH.MATH-PR]Mathematics [math]/Probability [math.PR], observability, [MATH.MATH-DG]Mathematics [math]/Differential Geometry [math.DG], General Mathematics, random set, [MATH.MATH-AP]Mathematics [math]/Analysis of PDEs [math.AP], wave equation, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], Riemannian geometry
Abstract: Given any measurable subset $\omega$ of a closed Riemannian manifold $(M,g)$ and given any $T>0$, we define $\ell^T(\omega)\in[0,1]$ as the smallest average time over $[0,T]$ spent by all geodesic rays in $\omega$. This quantity appears naturally when studying observability properties for the wave equation on $M$, with $\omega$ as an observation subset: the condition $\ell^T(\omega)>0$ is the well known \emph{Geometric Control Condition}.In this article we establish two properties of the functional $\ell^T$, one is geometric and the other is probabilistic.The first geometric property is on the maximal discrepancy of $\ell^T$ when taking the closure. We may have $\ell^T(\mathring{\omega})1/2$ then the Geometric Control Condition is satisfied and thus the wave equation is observable on $\omega$ in time $T$. The second property is of probabilistic nature. We take $M=\mathbb{T}^2$, the flat two-dimensional torus, and we consider a regular grid on it, a regular checkerboard made of $n^2$ square white cells. We construct random subsets $\omega_\varepsilon^n$ by darkening each cell in this grid with a probability $\varepsilon$. We prove that the random law $\ell^T(\omega_\varepsilon^n)$ converges in probability to $\varepsilon$ as $n\rightarrow+\infty$.As a consequence, if $n$ is large enough then the Geometric Control Condition is satisfied almost surely and thus the wave equation is observable on $\omega_\varepsilon^n$ in time $T$.
Published: 2022
Full Text: View/download PDF

7. A Posthumous Contribution by Larry Wos: Excerpts from an Unpublished Column

Author: Sophie Tourret, Christoph Weidenbach, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), and Max Planck Institute for Informatics [Saarbrücken]
Subjects: History of automated reasoning, Reasoning by instantiation, Puzzle, Computational Theory and Mathematics, Artificial Intelligence, First-order logic modulo arithmetic, Set of support, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Software
Abstract: Shortly before Larry Wos passed away, he sent a manuscript for discussion to Sophie Tourret, the editor of the AAR newsletter. We present excerpts from this final manuscript, put it in its historic context and explain its relevance for today’s research in automated reasoning.
Published: 2022
Full Text: View/download PDF

8. Reducing the memory usage of Lattice-Boltzmann schemes with a DWT-based compression

Author: Flint, Clément, Helluy, Philippe, Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (ICube), École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Les Hôpitaux Universitaires de Strasbourg (HUS)-Centre National de la Recherche Scientifique (CNRS)-Matériaux et Nanosciences Grand-Est (MNGE), Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Réseau nanophotonique et optique, Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), Compilation pour les Architectures MUlti-coeurS (CAMUS), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (ICube), Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Les Hôpitaux Universitaires de Strasbourg (HUS)-Centre National de la Recherche Scientifique (CNRS)-Matériaux et Nanosciences Grand-Est (MNGE), Institut de Recherche Mathématique Avancée (IRMA), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), TOkamaks and NUmerical Simulations (TONUS), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, and Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: [INFO.INFO-AR]Computer Science [cs]/Hardware Architecture [cs.AR], FOS: Computer and information sciences, LBM algorithm, GPU Graphic Processor, Stencil computation, [SCCO.COMP]Cognitive science/Computer science, Data Compression, Computer Science - Distributed, Parallel, and Cluster Computing, [MATH.MATH-MP]Mathematics [math]/Mathematical Physics [math-ph], HPC, Hardware Architecture (cs.AR), Distributed, Parallel, and Cluster Computing (cs.DC), [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], DWT, Computer Science - Hardware Architecture
Abstract: This paper presents a new solution to address the challenge of increasing memory usage in high-performance computing simulations of Lattice-Bolzmann or Finite-Volume schemes.Our approach utilises a lossy compression scheme based on the Discrete Wavelet Transform (DWT) to achieve high compression ratios while preserving the accuracy of the simulation.Our evaluation on two different FV/LBM schemes demonstrates that the approach can reduce memory usage by several orders of magnitude.; Ce papier présente une nouvelle solution pour faire face à l'augmentation de l'utilisation de la mémoire dans les simulations haute performance basées sur les méthodes Lattice-Bolzmann ou Volumes Finis.Notre approche utilise un schéma de compression avec perte basé sur la transformée par ondelettes discrète (DWT) pour obtenir des taux de compression élevés tout en préservant la précision de la simulation.Notre évaluation sur deux différents schémas VF/LBM démontre que l'approche peut réduire l'utilisation de la mémoire de plusieurs ordres de grandeur.
Published: 2023

9. Optimisation of the total population size for logistic diffusive equations: bang-bang property and fragmentation rate

Author: Idriss Mazari, Grégoire Nadin, Yannick Privat, Institute for Analysis and Scientific Computing [Wien], Vienna University of Technology (TU Wien), Laboratoire Jacques-Louis Lions (LJLL (UMR_7598)), Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP), Institut de Recherche Mathématique Avancée (IRMA), Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA), TOkamaks and NUmerical Simulations (TONUS), Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), I Mazari was partially supported by the Austrian Science Fund (FWF) projects I4052-N32 and F65. I. Mazari, G. Nadin and Y. Privat were partially supported by the Project 'Analysis and simulation of optimal shapes - application to lifesciences' of the Paris City Hall., ANR-18-CE40-0013,SHAPO,Optimisation de forme(2018), CEntre de REcherches en MAthématiques de la DEcision (CEREMADE), Université Paris Dauphine-PSL, Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Centre National de la Recherche Scientifique (CNRS), Université Paris sciences et lettres (PSL), Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut Universitaire de France (IUF), and Ministère de l'Education nationale, de l’Enseignement supérieur et de la Recherche (M.E.N.E.S.R.)
Subjects: Applied Mathematics, shape optimization, 010102 general mathematics, calculus of variations, bilinear optimal control, 01 natural sciences, 010101 applied mathematics, optimal control, 35Q92,49J99,34B15, Mathematics - Analysis of PDEs, Optimization and Control (math.OC), FOS: Mathematics, [MATH.MATH-AP]Mathematics [math]/Analysis of PDEs [math.AP], AMS: 35Q92,49J99,34B15, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], 0101 mathematics, diffusive logistic equation, Mathematics - Optimization and Control, Analysis, Analysis of PDEs (math.AP)
Abstract: International audience; In this article, we give an in-depth analysis of the problem of optimising the total population size for a standard logistic-diffusive model. This optimisation problem stems from the study of spatial ecology and amounts to the following question: assuming a species evolves in a domain, what is the best way to spread resources in order to ensure a maximal population size at equilibrium? {In recent years, many authors contributed to this topic.} We settle here the proof of two fundamental properties of optimisers: the bang-bang one which had so far only been proved under several strong assumptions, and the other one is the fragmentation of maximisers. Here, we prove the bang-bang property in all generality using a new spectral method. The technique introduced to demonstrate the bang-bang character of optimizers can be adapted and generalized to many optimization problems with other classes of bilinear optimal control problems where the state equation is semilinear and elliptic. We comment on it in a conclusion section.Regarding the geometry of maximisers, we exhibit a blow-up rate for the $BV$-norm of maximisers as the diffusivity gets smaller: if $\Omega$ is an orthotope and if $m_\mu$ is an optimal control, then $\Vert m_\mu\Vert_{BV}\gtrsim \sqrt{\mu}$. The proof of this results relies on a very fine energy argument.
Published: 2021
Full Text: View/download PDF

10. Parallel kinetic scheme in complex toroidal geometry

Author: Boileau, Matthieu, Bramas, Bérenger, Franck, Emmanuel, Hélie, Romane, Helluy, Philippe, Navoret, Laurent, Institut de Recherche Mathématique Avancée (IRMA), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), TOkamaks and NUmerical Simulations (TONUS), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Compilation pour les Architectures MUlti-coeurS (CAMUS), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (ICube), École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Les Hôpitaux Universitaires de Strasbourg (HUS)-Centre National de la Recherche Scientifique (CNRS)-Matériaux et Nanosciences Grand-Est (MNGE), Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Réseau nanophotonique et optique, Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Les Hôpitaux Universitaires de Strasbourg (HUS)-Centre National de la Recherche Scientifique (CNRS)-Matériaux et Nanosciences Grand-Est (MNGE), Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), and Helluy, Philippe
Subjects: 35L65, 65M12, 35Q83, 82D10, Physics::Plasma Physics, plasma physics, [MATH.MATH-AP]Mathematics [math]/Analysis of PDEs [math.AP], [MATH.MATH-AP] Mathematics [math]/Analysis of PDEs [math.AP], kinetic scheme, discontinuous Galerkin
Abstract: We present an efficient solver for the conservative transport equation with variable coefficients in complex toroidal geometries. The solver is based on a kinetic formulation resembling the Lattice-Boltzmann approach.The chosen formalism allows to obtain an explicit and conservative scheme that requires no matrix inversion and whose CFL stability condition is independent from the poloidal dynamics. We present the method and its optimized parallel implementation on toroidal geometries. Two and three dimensional plasma physics test cases are carried out.
Published: 2022
Full Text: View/download PDF

11. Gridless 3D Recovery of Image Sources from Room Impulse Responses

Author: Tom Sprunck, Antoine Deleforge, Yannick Privat, Cedric Foy, Institut de Recherche Mathématique Avancée (IRMA), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), TOkamaks and NUmerical Simulations (TONUS), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Speech Modeling for Facilitating Oral-Based Communication (MULTISPEECH), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Natural Language Processing & Knowledge Discovery (LORIA - NLPKD), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Unité Mixte de Recherche en Acoustique Environnementale (UMRAE ), Centre d'Etudes et d'Expertise sur les Risques, l'Environnement, la Mobilité et l'Aménagement (Cerema)-Université Gustave Eiffel, and ANR-20-CE48-0013,DENISE,Attaque de problèmes difficiles en audio par des approches inverses non-linéaires économes en données(2020)
Subjects: Signal Processing (eess.SP), FOS: Computer and information sciences, Sound (cs.SD), Acoustic reflectors, convex optimization, room shape, Applied Mathematics, Classical Physics (physics.class-ph), FOS: Physical sciences, super-resolution, Physics - Classical Physics, sound field, Computer Science - Sound, [PHYS.MECA.ACOU]Physics [physics]/Mechanics [physics]/Acoustics [physics.class-ph], [INFO.INFO-TS]Computer Science [cs]/Signal and Image Processing, Audio and Speech Processing (eess.AS), Signal Processing, [INFO.INFO-SD]Computer Science [cs]/Sound [cs.SD], FOS: Electrical engineering, electronic engineering, information engineering, Electrical Engineering and Systems Science - Signal Processing, Electrical and Electronic Engineering, Electrical Engineering and Systems Science - Audio and Speech Processing, sliding Frank-Wolfe
Abstract: Given a sound field generated by a sparse distribution of impulse image sources, can the continuous 3D positions and amplitudes of these sources be recovered from discrete, bandlimited measurements of the field at a finite set of locations, e.g., a multichannel room impulse response? Borrowing from recent advances in super-resolution imaging, it is shown that this nonlinear, non-convex inverse problem can be efficiently relaxed into a convex linear inverse problem over the space of Radon measures in R3. The linear operator introduced here stems from the fundamental solution of the free-field inhomogenous wave equation combined with the receivers' responses. An adaptation of the Sliding Frank-Wolfe algorithm is proposed to numerically solve the problem off-the-grid, i.e., in continuous 3D space. Simulated experiments show that the approach achieves near-exact recovery of hundreds of image sources using an arbitrarily placed compact 32-channel spherical microphone array in random rectangular rooms. The impact of noise, sampling rate and array diameter on these results is also examined., Comment: IEEE Signal Processing Letters, 2022
Published: 2022
Full Text: View/download PDF

12. A Comprehensive Framework for Saturation Theorem Proving

Author: Waldmann, Uwe, Tourret, Sophie, Robillard, Simon, Blanchette, Jasmin, Peltier, Nicolas, Sofronie-Stokkermans, Viorica, Theoretical Computer Science, Network Institute, Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Département Automatique, Productique et Informatique (IMT Atlantique - DAPI), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Vrije Universiteit Amsterdam [Amsterdam] (VU), Proof-oriented development of computer-based systems (MOSEL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Peltier, Nicolas, Sofronie-Stokkermans, Viorica, Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), Université de Montpellier (UM), and IMT Atlantique (IMT Atlantique)
Subjects: Computer science, Prover architectures, 02 engineering and technology, Gas meter prover, Mathematical proof, Article, Image (mathematics), Automated theorem proving Saturation Resolution calculus Superposition calculus Redundancy Prover architectures, Redundancy, Artificial Intelligence, Completeness (order theory), 0202 electrical engineering, electronic engineering, information engineering, Calculus, Redundancy (engineering), Automated theorem proving, Superposition calculus, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Resolution (logic), Saturation, Resolution calculus, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Cover (topology), Computational Theory and Mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, 020201 artificial intelligence & image processing, Software
Abstract: A crucial operation of saturation theorem provers is deletion of subsumed formulas. Designers of proof calculi, however, usually discuss this only informally, and the rare formal expositions tend to be clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but the standard notion of redundancy is too weak: A clause C does not make an instance $$C\sigma $$ C σ redundant. We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution and superposition. The framework modularly extends redundancy criteria derived via a familiar ground-to-nonground lifting. It allows us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures so that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of a prover implementing the calculus within, for instance, an Otter or DISCOUNT loop. Our framework is mechanized in Isabelle/HOL.
Published: 2022
Full Text: View/download PDF

13. Making Higher-Order Superposition Work

Author: Vukmirović, P., Bentkamp, A., Blanchette, J., Cruanes, S., Nummelin, V., Tourret, S., Platzer, André, Sutcliffe, Geoff, Vrije Universiteit Amsterdam [Amsterdam] (VU), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Aesthetic Integration, Theoretical Computer Science, Network Institute, Computer Science, Computer Systems Section - Vrije Universiteit Amsterdam, Max-Planck-Gesellschaft, Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Platzer, André, Sutcliffe, Geoff, Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), and Max-Planck-Gesellschaft-Max-Planck-Gesellschaft
Subjects: Higher-order theorem proving, Theoretical computer science, Computer science, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, Branching (linguistics), Competition (economics), Superposition principle, Artificial Intelligence, Order (exchange), 0202 electrical engineering, electronic engineering, information engineering, Heuristics, SDG 7 - Affordable and Clean Energy, 0101 mathematics, Rule of inference, Superposition, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, Extension (predicate logic), Division (mathematics), Automated theorem proving, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, 010201 computation theory & mathematics, 020201 artificial intelligence & image processing, Zipperposition, Software
Abstract: This archive contains the raw evaluation results and scripts associated with the experiments described in the article "Making Higher-Order Superposition Work" by Vukmirović, Bentkamp, Blanchette, Cruanes, Nummelin and Tourret available at: https://matryoshka-project.github.io/pubs/mhosw_article.pdf The problems we used for the evaluation are in problems/ subdirectory, divided in categories sh and tptp as in the article. In the results/ directory there are two subdirectories, sh and tptp, one for each benchmark category. Both subdirectories contain files named fD.csv where D is a number from 1 to 10. The files contain experiment results for the figure labelled with the number D, and the benchmark category corresponding to the parent directory. In the result files, the columns give the results of the experiment run for a given prover configuration (e.g., CPU time, reported status, memory usage, etc.). Each row corresponds to one problem file, whose name is given in the "prob_name" column. The "i_solver" column corresponds to a prover, whereas the "i_configuration" column corresponds to a configuration, where i is a natural number identifying a combination of prover and configuration. Files ending with "summary.csv" contain concise summaries of evaluation runs for a corresponding results file. Columns of these files are of the form "{solver}_{configuration}", and rows contain different statistics described in the "summary" column. The names of the solvers and configurations used in result files are self-explanatory (for DCS, DCI and IC configurations presence of av in the name of the configuration denotes that Avatar is enabled). In some cases, for uniformity, configurations are used in multiple figures. We used the following versions of higher-order provers: CVC4 1.9 ([git cascJ10 db26022c]), Leo-III 1.5.6, Satallax 3.5, Vampire 4.5.1 (commit 68d3e7314), E 2.7 (603992156b943171002cacca72aa3f2d0a211ee3). The "zipperposition/" directory contains the scripts that can be used to run the provided Zipperposition binary (compiled for Linux) on a given problem using a given configuration. To run Zipperposition on a single problem using some configuration, use the scripts with the name "run_*", where * stands for the configuration used in the evaluation. The configuration names match those used in the result files. Except for "run_coop" and "run_uncoop", scripts accept three arguments: 1) path to the problem 2) CPU timeout 3) path to the temporary directory for files used to communicate with Ehoh. "run_coop" and "run_uncoop" expect only the first two arguments For example, to run problem with the path ~/problem.p using configuration which enables PEHO priority function for up to 15 seconds execute ./run_prio_peho ~/problem.p 15 /tmp Working installation of Python 3 and bash is required. Source code for Zipperposition can be obtained from the wip-merge-hlbe branch of Zipperposition git repository: git@github.com:sneeuwballen/zipperposition.git. The binary stored under scripts/ directory corresponds to compiled sources tagged with commit hash 8d205ecf8869c76dcfdf0c1faa98b002226780a1. Compilation instructions are as in README.md file contained in the git repository. As noted in footnote 2, three tables have been evaluated using a faulty version of Ehoh prover. Reevaluation is being performed, and it is expected that the evaluation results will stay mostly the same, up to the noise in the evaluation environment. "eprover-ho" binary provided in this archive is the corrected version of the one used to evaluate tables 7, 8 and 9.
Published: 2022
Full Text: View/download PDF

14. Shape and topology optimization for maximum probability domains in quantum chemistry

Author: Braida, Benoît, Dalphin, Jérémy, Dapogny, Charles, Frey, Pascal, Privat, Yannick, Laboratoire de chimie théorique (LCT), Institut de Chimie du CNRS (INC)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS), Institut des Sciences du Calcul et des Données (ISCD), Sorbonne Université (SU), Equations aux Dérivées Partielles (EDP), Laboratoire Jean Kuntzmann (LJK), Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), TOkamaks and NUmerical Simulations (TONUS), Institut de Recherche Mathématique Avancée (IRMA), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), Institut Universitaire de France (IUF), Ministère de l'Education nationale, de l’Enseignement supérieur et de la Recherche (M.E.N.E.S.R.), The work of Charles Dapogny and Yannick Privat is partly supported by the project ANR-18-CE40-0013 SHAPO, financed by the French Agence Nationale de la Recherche (ANR)., ANR-18-CE40-0013,SHAPO,Optimisation de forme(2018), Calcul des Variations, Géométrie, Image (CVGI), Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Inria Nancy - Grand Est, and Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)
Subjects: Computational Mathematics, Maximum Probability Domains, AMS classification: 35P20, 93B07, 58J51, 49K20, Applied Mathematics, Fixed Point Algorithm, Shape Optimization, Level Set Method, [MATH.MATH-AP]Mathematics [math]/Analysis of PDEs [math.AP], [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], Quantum Chemistry
Abstract: International audience; This article is devoted to the mathematical and numerical treatments of a shape optimization problem emanating from the desire to reconcile quantum theories of chemistry and classical heuristic models: we aim to identify Maximum Probability Domains (MPDs), that is, domains $\Omega$ of the 3d space where the probability $\mathbb{P}_\nu(\Omega)$ to find exactly $\nu$ among the $n$ constituent electrons of a given molecule is maximum. In the Hartree-Fock framework, the shape functional $\mathbb{P}_\nu(\Omega)$ arises as the integral over $\nu$ copies of $\Omega$ and $(n-\nu)$ copies of the complement $\mathbb{R}^3 \setminus \Omega$ of an analytic function defined over the space $\mathbb{R}^{3n}$ of all the spatial configurations of the $n$ electron system. Our first task is to explore the mathematical well-posedness of the shape optimization problem: under mild hypotheses, we prove that global maximizers of the probability functions $\mathbb{P}_\nu(\Omega)$ do exist as open subsets of $\mathbb{R}^3$; meanwhile, we identify the associated necessary first-order optimality condition. We then turn to the numerical calculation of MPDs, for which we resort to a level set based mesh evolution strategy: the latter allows for the robust tracking of complex evolutions of shapes, while leaving the room for accurate chemical computations, carried out on high-resolution meshes of the optimized shapes. The efficiency of this procedure is enhanced thanks to the addition of a fixed-point strategy inspired from the first-order optimality conditions resulting from our theoretical considerations. Several three-dimensional examples are presented and discussed to appraise the efficiency of our algorithms.
Published: 2022
Full Text: View/download PDF

15. Parallelization of the Lattice-Boltzmann schemes using the task-based method

Author: Flint, Clément, Bramas, Berenger, Genaud, Stephane, Helluy, Philippe, Laboratoire de Sciences de l'Image, de l'Informatique et de la Télédétection, équipe ICPS (LSIIT / ICPS), Université Louis Pasteur - Strasbourg I-Centre National de la Recherche Scientifique (CNRS), Compilation pour les Architectures MUlti-coeurS (CAMUS), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (ICube), École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Les Hôpitaux Universitaires de Strasbourg (HUS)-Centre National de la Recherche Scientifique (CNRS)-Matériaux et Nanosciences Grand-Est (MNGE), Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Réseau nanophotonique et optique, Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Les Hôpitaux Universitaires de Strasbourg (HUS)-Centre National de la Recherche Scientifique (CNRS)-Matériaux et Nanosciences Grand-Est (MNGE), Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), TOkamaks and NUmerical Simulations (TONUS), Institut de Recherche Mathématique Avancée (IRMA), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS), and Bramas, Bérenger
Subjects: [INFO.INFO-DC] Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC]
Abstract: National audience; The popularization of graphic processing units (GPUs) has led to their extensive use in highperformance numerical simulations. The Lattice Boltzmann Methodology (LBM) is a general framework for constructing efficient numerical fluid simulations. In this scheme, the fluid quantities are approximated on a structured grid. At each time step, a shift-relaxation process is applied, where each kinetic value is shifted to the corresponding direction in the lattice. Thanks to its simplicity, the LBM is subject to many software optimizations. State-of-the-art techniques aim at adapting the LBM scheme to improve the computational throughput on modern processors. Currently, most effort is put into optimizing this process on GPUs, as their architecture is highly suited for this type of computation. A bottleneck of GPU implementations is that the data size of the simulation is limited by the GPU memory. This restricts the number of volume elements and, therefore, the degree of precision one can obtain. In this work, we divide the lattice structure into multiple subsets that can be executed individually. This allows the work to be distributed among different processing units at the cost of increased complexity and memory transfers. But the constraint on GPU memory is relaxed, as the subsets can be made as small as needed. Additionally, we use the task-based approach for parallelizing the application, which allows the computation to be efficiently distributed among multiple processing units.
Published: 2022

16. An Approximation of Minimax Control using Random Sampling and Symbolic Computation

Author: Étienne André, Laurent Fribourg, Jawher Jerray, Laboratoire d'Informatique de Paris-Nord (LIPN), Centre National de la Recherche Scientifique (CNRS)-Université Sorbonne Paris Nord, Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), and Max-Planck-Gesellschaft-Max-Planck-Gesellschaft
Subjects: 0209 industrial biotechnology, 021103 operations research, bounded uncertainty, random sampling, 0211 other engineering and technologies, Euler's method, Perturbation (astronomy), Value (computer science), 02 engineering and technology, State (functional analysis), Symbolic computation, Minimax, Domain (mathematical analysis), optimal control, 020901 industrial engineering & automation, Control and Systems Engineering, Bounded function, [INFO.INFO-SY]Computer Science [cs]/Systems and Control [cs.SY], Applied mathematics, Switched systems, SIMPLE algorithm, Mathematics
Abstract: This manuscript is published in the proceedings of the 7th IFAC Conference on Analysis and Design of Hybrid Systems (ADHS 2021).; International audience; We aim at the synthesis of an approximate minimax control for a system dynamic given in the form x.(t) = f(x(t),u(t),d(t)) where x represents the state, u the control (or input) and d a disturbance (or perturbation).The disturbance d(t) is prescribed to a compact domain D on which it can take any value (bounded uncertainty).Our method makes use of symbolic computation to enclose the solutions corresponding to all possible disturbance d. in D, together with a simple algorithm of random sampling to select the minimum control u*.We illustrate the interest of this approximate minimax control on an example of a biochemical reactor.
Published: 2021
Full Text: View/download PDF

17. Minimal cost-time strategies for mosquito population replacement

Author: Almeida, Luis, Bellver Arnau, Jesús, Duprez, Michel, Privat, Yannick, Laboratoire Jacques-Louis Lions (LJLL (UMR_7598)), Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Modelling and Analysis for Medical and Biological Applications (MAMBA), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Jacques-Louis Lions (LJLL (UMR_7598)), Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), Computational Anatomy and Simulation for Medicine (MIMESIS), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (ICube), École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Institut National de Recherche en Informatique et en Automatique (Inria)-Les Hôpitaux Universitaires de Strasbourg (HUS)-Centre National de la Recherche Scientifique (CNRS)-Matériaux et Nanosciences Grand-Est (MNGE), Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Institut National de la Santé et de la Recherche Médicale (INSERM)-Institut de Chimie du CNRS (INC)-Centre National de la Recherche Scientifique (CNRS)-Réseau nanophotonique et optique, Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-École Nationale du Génie de l'Eau et de l'Environnement de Strasbourg (ENGEES)-Université de Strasbourg (UNISTRA)-Institut National des Sciences Appliquées - Strasbourg (INSA Strasbourg), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Les Hôpitaux Universitaires de Strasbourg (HUS)-Centre National de la Recherche Scientifique (CNRS)-Matériaux et Nanosciences Grand-Est (MNGE), Université de Strasbourg (UNISTRA)-Université de Haute-Alsace (UHA) Mulhouse - Colmar (Université de Haute-Alsace (UHA))-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), Laboratoire des sciences de l'ingénieur, de l'informatique et de l'imagerie (ICube), TOkamaks and NUmerical Simulations (TONUS), Institut de Recherche Mathématique Avancée (IRMA), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), This research was supported by the Project 'Analysis and simulation of optimal shapes - applicationto life science' of the Paris City Hall., Roland Herzog, Matthias Heinkenschloss, Dante Kalise, and Georg Stadler and Emmanuel Trélat
Subjects: parasitic diseases, [MATH.MATH-AP]Mathematics [math]/Analysis of PDEs [math.AP], Ordinary differential systems, Minimal time, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], Wolbachia, Optimal control, Epidemic vector control
Abstract: International audience; Vector control plays a central role in the fight against vector-borne diseases and, in particular, arboviruses. The use of the endosymbiotic bacterium \textit{Wolbachia} has proven effective in preventing the transmission of some of these viruses between mosquitoes and humans, making it a promising control tool. The population replacement technique we consider consists in replacing the wild population by a population carrying the aforementioned bacterium, thereby preventing outbreaks of the associated vector-borne diseases.In this work, we consider a two species model incorporating both Wolbachia infected and wild mosquitoes. Our system can be controlled thanks to a term representing an artificial introduction of Wolbachia-infected mosquitoes. Under the assumption that the birth rate of mosquitoes is high, we may reduce the model to a simpler one regarding the proportion of infected mosquitoes. We investigate minimal cost-time strategies to achieve a population replacement both analytically and numerically for the simplified 1D model and only numerically for the full 2D system.
Published: 2022
Full Text: View/download PDF

18. Freely orientable microstructures for designing deformable 3D prints

Author: Jonàs Martínez, Fabrice Neyret, Sylvain Lefebvre, Cédric Zanni, Pierre-Alexandre Hugron, Thibault Tricard, Vincent Tavernier, Matter from Graphics (MFX), Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), Models and Algorithms for Visualization and Rendering (MAVERICK), Inria Grenoble - Rhône-Alpes, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Jean Kuntzmann (LJK), Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA)-Centre National de la Recherche Scientifique (CNRS)-Université Grenoble Alpes (UGA)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP ), Université Grenoble Alpes (UGA), This work was supported partly by the french PIA project « Lorraine Université d’Excellence » (ANR-15-IDEX-04-LUE), by the ANRMuFFin (ANR-17-CE10-0002), and the project IMPRIMA (ANR-18-CE46-0004)., ANR-17-CE10-0002,MuFFin,Microstructures procedurales et stochastiques pour la fabrication fonctionnelle(2017), ANR-15-IDEX-0004,LUE,Isite LUE(2015), ANR-18-CE46-0004,IMPRIMA,Modélisation par surface implicite pour la fabrication additive(2018), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)
Subjects: noise, Fabrication, Materials science, business.industry, Acoustics, Isotropy, 3D printing, 020207 software engineering, Rigidity (psychology), 02 engineering and technology, phasor, Deformation (meteorology), textures, [INFO.INFO-CG]Computer Science [cs]/Computational Geometry [cs.CG], Computer Graphics and Computer-Aided Design, Computing methodologies, Simple (abstract algebra), procedural, Orientation (geometry), 0202 electrical engineering, electronic engineering, information engineering, Procedural texture, business
Abstract: Nature offers a marvel of astonishing and rich deformation behaviors. Yet, most of the objects we fabricate are comparatively rather inexpressive, either rigid or exhibiting simple homogeneous deformations when interacted with. We explore the synthesis and fabrication of novel microstructures that mimic the effects of having oriented rigid fibers in an otherwise flexible material: the result is extremely rigid along a transverse direction while being comparatively very flexible in the locally orthogonal plane. By allowing free gradation of the rigidity direction orientation within the object, the microstructures can be designed such that, under deformation, distances along fibers in the volume are preserved while others freely change. Through a simple painting tool, this allows a designer to influence the way the volume reshapes when deformed, and results in a wide range of novel possibilities. Many gradations are possible: local free orientation of the fibers; local control of the overall material rigidity (structure density); local canceling of the effect of the fibers, obtaining a more isotropic material. Our algorithm to synthesize the structures builds upon procedural texturing. It produces a cellular geometry that can be fabricated reliably despite 3D printing walls at a minimal thickness, allowing prints to be very flexible. The synthesis algorithm is efficient and scales to large volumes.
Published: 2020
Full Text: View/download PDF

19. A complete and terminating approach to linear integer solving

Author: Thomas Sturm, Martin Bromberger, Christoph Weidenbach, Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Saarland University [Saarbrücken], Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, and Universität des Saarlandes [Saarbrücken]
Subjects: Normalization property, CDCL, Algebra and Number Theory, 010102 general mathematics, Linear arithmetic, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Context (language use), 010103 numerical & computational mathematics, Integer arithmetic, Space (mathematics), 01 natural sciences, Satisfiability, Decidability, Algebra, Computational Mathematics, SMT, Linear programming, Quantifier elimination, Order (group theory), SAT, [INFO]Computer Science [cs], 0101 mathematics, Integer (computer science), Mathematics
Abstract: International audience; We consider feasibility of linear integer problems in the context of verification systems such as SMT solvers or theorem provers. Although satisfiability of linear integer problems is decidable, many state-of-the-art implementations neglect termination in favor of efficiency. We present thecalculus CutSat++ that is sound, terminating, complete, and leaves enough space for model assumptions and simplification rules in order to be efficient in practice. CutSat++ combines model-driven reasoning and quantifier elimination to the feasibility of linear integer problems.
Published: 2020
Full Text: View/download PDF

20. Random polytopes and the wet part for arbitrary probability distributions

Author: Matthieu Fradelizi, Xavier Goaoc, Alfredo Hubard, Imre Bárány, Günter Rote, Alfréd Rényi Institute of Mathematics, Hungarian Academy of Sciences (MTA), Laboratoire d'Analyse et de Mathématiques Appliquées (LAMA), Université Paris-Est Marne-la-Vallée (UPEM)-Fédération de Recherche Bézout-Université Paris-Est Créteil Val-de-Marne - Paris 12 (UPEC UP12)-Centre National de la Recherche Scientifique (CNRS), Geometric Algorithms and Models Beyond the Linear and Euclidean realm (GAMBLE ), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Laboratoire d'Informatique Gaspard-Monge (ligm), Université Paris-Est Marne-la-Vallée (UPEM)-École des Ponts ParisTech (ENPC)-ESIEE Paris-Fédération de Recherche Bézout-Centre National de la Recherche Scientifique (CNRS), Institut für Informatik [Berlin], Freie Universität Berlin, Rényi Institute of Mathematics, University College London, Université Paris-Est, Université de Lorraine, ANR-17-CE40-0017,ASPAG,Analyse et Simulation Probabilistes des Algorithmes Géométriques(2017), Centre National de la Recherche Scientifique (CNRS)-Université Paris-Est Créteil Val-de-Marne - Paris 12 (UPEC UP12)-Fédération de Recherche Bézout-Université Paris-Est Marne-la-Vallée (UPEM), Laboratoire d'Informatique Gaspard-Monge (LIGM), Centre National de la Recherche Scientifique (CNRS)-Fédération de Recherche Bézout-ESIEE Paris-École des Ponts ParisTech (ENPC)-Université Paris-Est Marne-la-Vallée (UPEM), Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), Goaoc, Xavier, Analyse et Simulation Probabilistes des Algorithmes Géométriques - - ASPAG2017 - ANR-17-CE40-0017 - AAPG2017 - VALID, Imre. Barany was supported by the Hungarian National Research, Development and Innovation Office NKFIH Grants K 111827 andK 116769, and by the Bézout Labex (ANR-10-LABX-58). Xavier Goaoc was supported by Institut Universitaire de France. The authors are grateful for the hospitality during the ASPAG (ANR-17-CE40-0017) workshop on geometry, probability, and algorithms in Arcachon in April 2018., ANR-10-LABX-0058,Bézout,Models and algorithms: from the discrete to the continuous(2010), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est
Subjects: Convex hull, [MATH.MATH-PR] Mathematics [math]/Probability [math.PR], Uniform distribution (continuous), Random polytopes, Convex set, Ocean Engineering, Polytope, [MATH] Mathematics [math], 01 natural sciences, Measure (mathematics), Upper and lower bounds, Combinatorics, 010104 statistics & probability, FOS: Mathematics, Mathematics::Metric Geometry, 60D05, [MATH]Mathematics [math], 0101 mathematics, Mathematics, Probability measure, Epsilon-nets, Probability (math.PR), 010102 general mathematics, [MATH.MATH-PR]Mathematics [math]/Probability [math.PR], Floating body, Probability distribution, Mathematics - Probability
Abstract: We examine how the measure and the number of vertices of the convex hull of a random sample of $n$ points from an arbitrary probability measure in $\mathbf{R}^d$ relates to the wet part of that measure. This extends classical results for the uniform distribution from a convex set [B\'ar\'any and Larman 1988]. The lower bound of B\'ar\'any and Larman continues to hold in the general setting, but the upper bound must be relaxed by a factor of $\log n$. We show by an example that this is tight., Comment: 13 pages, 1 figure
Published: 2020
Full Text: View/download PDF

21. Anisotropic Soft Robots Based on 3D Printed Meso-Structured Materials: Design, Modeling by Homogenization and Simulation

Author: Olivier Goury, Jonàs Martínez, Hervé Delingette, Christian Duriez, Sylvain Lefebvre, Felix Vanneste, Deformable Robots Simulation Team (DEFROST ), Inria Lille - Nord Europe, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 (CRIStAL), Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Centrale Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Geometry and Lighting (ALICE), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Matter from Graphics (MFX), COMUE Université Côte d'Azur (2015-2019) (COMUE UCA), Hauts de France Region, SOFA, ANR-17-CE10-0002,MuFFin,Microstructures procedurales et stochastiques pour la fabrication fonctionnelle(2017), Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189 (CRIStAL), Ecole Centrale de Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189 (CRIStAL), Ecole Centrale de Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS)-Ecole Centrale de Lille-Université de Lille-Centre National de la Recherche Scientifique (CNRS), Université Côte d'Azur (UCA), Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, and Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: 0209 industrial biotechnology, 3d printed, Kinematics, Control and Optimization, Computer science, Additive Manufacturing, Simulation and Animation, Biomedical Engineering, Mechanical engineering, 02 engineering and technology, Materials design, Homogenization (chemistry), 020901 industrial engineering & automation, Artificial Intelligence, 0202 electrical engineering, electronic engineering, information engineering, medicine, [INFO.INFO-RB]Computer Science [cs]/Robotics [cs.RO], Anisotropy, ComputingMethodologies_COMPUTERGRAPHICS, Mechanical Engineering, Stiffness, 020207 software engineering, Soft Robot Applications, [INFO.INFO-MO]Computer Science [cs]/Modeling and Simulation, Finite element method, Computer Science Applications, Human-Computer Interaction, Control and Systems Engineering, Robot, Computer Vision and Pattern Recognition, medicine.symptom, Soft Robot Materials and Design
Abstract: International audience; In this paper, we propose to use new 3D-printed meso-structured materials to build soft robots and we present a modeling pipeline for design assistance and control. These meta-materials can be programmed before printing to target specific mechanical properties, in particular heterogeneous stiffness and anisotropic behaviour. Without changing the external shape, we show that using such meta-material can lead to a dramatic change in the kinematics of the robot. This highlights the importance of modeling. Therefore, to help the design and to control soft robots made of these meso-structured materials, we present a modeling method based on numerical homogenization and Finite Element Method (FEM) that captures the anisotropic deformations. The method is tested on a 3 axis parallel soft robot initially made of silicone. We demonstrate the change in kinematics when the robot is built with meso-structured materials and compare its behavior with modeling results.
Published: 2020
Full Text: View/download PDF

22. An asynchronous cellular system that solves the parity problem

Author: Fatès, Nazim, Designing the Future of Computational Models (MOCQUA), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and Inria Nancy Grand-Est
Subjects: [NLIN.NLIN-CG]Nonlinear Sciences [physics]/Cellular Automata and Lattice Gases [nlin.CG]
Abstract: We present stochastic solutions to the cellular automata parity problem. The model is an interacting particles system where cells are updated by pairs, randomly chosen at each time step. We analyse the convergence properties of two rules and show that they possess the required properties to classify the parity of the initial configurations. We present a formal analysis of the classification time, as well as numerical simulations, to establish that the classification time scales quadratically with the number of cells.
Published: 2022

23. Families of SNARK-Friendly 2-Chains of Elliptic Curves

Author: Youssef El Housni, Aurore Guillevic, Geometry, arithmetic, algorithms, codes and encryption (GRACE), Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), ConsenSys, Aarhus University [Aarhus], Cryptology, arithmetic : algebraic methods for better algorithms (CARAMBA), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Colin Boyd, Orr Dunkelman, Stefan Dziembowski, Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X)-Inria Saclay - Ile de France, Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, and Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: International audience; At CANS'20, El Housni and Guillevic introduced a new 2-chain of pairing-friendly elliptic curves for recursive zero-knowledge Succinct Non-interactive ARguments of Knowledge (zk-SNARKs) made of the former BLS12-377 curve (a Barreto–Lynn–Scott curve over a 377-bit prime field) and the new BW6-761 curve (a Brezing–Weng curve of embedding degree 6 over a 761-bit prime field). First we generalise the curve construction, the pairing formulas (e : G1 × G2 → GT) and the group operations to any BW6 curve defined on top of any BLS12 curve, forming a family of 2-chain pairing-friendly curves.Second, we investigate other possible 2-chain families made on top of the BLS12 and BLS24 curves. We compare BW6 to Cocks–Pinch curves of higher embedding degrees 8 and 12 (CP8, CP12) at the 128-bit security level. We derive formulas for efficient optimal ate and optimal Tate pairings on our new CP curves. We show that for both BLS12 and BLS24, the BW6 construction always gives the fastest pairing and curve arithmetic compared to Cocks–Pinch curves. Finally, we suggest a short list of curves suitable for Groth16 and KZG-based universal SNARKs and present an optimized implementation of these curves. Based on Groth16 and PlonK (a KZG-based SNARK) implementations in the gnark ecosystem, we obtain that the BLS12-377/BW6-761 pair is optimized for the former while the BLS24-315/BW6-672 pair is optimized for the latter.
Published: 2022
Full Text: View/download PDF

24. History of Cryptographic Key Sizes

Author: Smart, Nigel, Thomé, Emmanuel, IMEC (IMEC), Catholic University of Leuven - Katholieke Universiteit Leuven (KU Leuven), Cryptology, arithmetic : algebraic methods for better algorithms (CARAMBA), Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Joppe Bos, and Martijn Stam
Subjects: [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], ComputingMilieux_MISCELLANEOUS
Abstract: International audience
Published: 2022

25. Optimal shape of stellarators for magnetic confinement fusion

Author: Yannick Privat, Rémi Robin, Mario Sigalotti, Université de Strasbourg (UNISTRA), TOkamaks and NUmerical Simulations (TONUS), Institut de Recherche Mathématique Avancée (IRMA), Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire Jacques-Louis Lions (LJLL (UMR_7598)), Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP), Control And GEometry (CaGE ), Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Jacques-Louis Lions (LJLL (UMR_7598)), Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université de Paris (UP), AEX StellaCage, ANR-18-CE40-0013,SHAPO,Optimisation de forme(2018), ANR-20-CE40-0009,TRECOS,Nouvelles directions en contrôle et stabilisation: Contraintes et termes non-locaux(2020), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité), and Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité)-Sorbonne Université (SU)-Centre National de la Recherche Scientifique (CNRS)-Université Paris Cité (UPCité)
Subjects: Biot and Savart operator, Plasma Physics, Applied Mathematics, General Mathematics, FOS: Physical sciences, Physics - Plasma Physics, Plasma Physics (physics.plasm-ph), Riemannian manifolds, AMS classification (MSC 2020): 49Q10, 49Q12, 78A25, 65T40, Shape optimization, Optimization and Control (math.OC), [PHYS.PHYS.PHYS-PLASM-PH]Physics [physics]/Physics [physics]/Plasma Physics [physics.plasm-ph], FOS: Mathematics, [MATH.MATH-OC]Mathematics [math]/Optimization and Control [math.OC], Mathematics - Optimization and Control
Abstract: International audience; We are interested in the design of stellarators, devices for the production of controlled nuclear fusion reactions alternative to tokamaks. The confinement of the plasma is entirely achieved by a helical magnetic field created by the complex arrangement of coils fed by high currents around a toroidal domain. Such coils describe a surface called "coil winding surface" (CWS). In this paper, we model the design of the CWS as a shape optimization problem, so that the cost functional reflects both optimal plasma confinement properties, through a least square discrepancy, and also manufacturability, thanks to geometrical terms involving the lateral surface or the curvature of the CWS. We completely analyze the resulting problem: on the one hand, we establish the existence of an optimal shape, prove the shape differentiability of the criterion, and provide the expression of the differential in a workable form. On the other hand, we propose a numerical method and perform simulations of optimal stellarator shapes. We discuss the efficiency of our approach with respect to the literature in this area.
Published: 2021
Full Text: View/download PDF

26. CTET+: A Beyond-Birthday-Bound Secure Tweakable Enciphering Scheme Using a Single Pseudorandom Permutation

Author: Benoît Cogliati, Jordan Ethan, Virginie Lallemand, Byeonghak Lee, Jooyoung Lee, Marine Minier, Helmholtz Center for Information Security [Saarbrücken] (CISPA), Cryptology, arithmetic : algebraic methods for better algorithms (CARAMBA), Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), Korea Advanced Institute of Science and Technology (KAIST), We would like to thank the anonymous reviewers for their valuable suggestions that helped improving the paper. This work was carried out in the framework of the French-German-Center for Cybersecurity, a collaboration of CISPA and LORIA and was partly supported by the french PIA project 'Lorraine Université d’Excellence', reference ANR-15 IDEX-04-LUE. Jooyoung was supported by Institute for Information & communications Technology Planning & Evaluation(IITP) grant funded by the Korea government(MSIT) (No.2019-0-01343, Regional strategic industry convergence security core talent training business). Part of this work was written while Benoît Cogliati was employed by the University of Luxembourg., Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)
Subjects: TK7885-7895, Computer engineering. Computer hardware, Computational Mathematics, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Applied Mathematics, tweakable enciphering mode, beyond-birthday-bound security, SPN, Software, Computer Science Applications
Abstract: International audience; In this work, we propose a construction of 2-round tweakable substitution permutation networks using a single secret S-box. This construction is based on non-linear permutation layers using independent round keys, and achieves security beyond the birthday bound in the random permutation model. When instantiated with an n-bit block cipher with ωn-bit keys, the resulting tweakable block cipher, dubbed CTET+, can be viewed as a tweakable enciphering scheme that encrypts ωκ-bit messages for any integer ω ≥ 2 using 5n + κ-bit keys and n-bit tweaks, providing 2n/3-bit security. Compared to the 2-round non-linear SPN analyzed in [CDK+18], we both minimize it by requiring a single permutation, and weaken the requirements on the middle linear layer, allowing better performance. As a result, CTET+ becomes the first tweakable enciphering scheme that provides beyond-birthday-bound security using a single permutation, while its efficiency is still comparable to existing schemes including AES-XTS, EME, XCB and TET. Furthermore, we propose a new tweakable enciphering scheme, dubbed AES6-CTET+, which is an actual instantiation of CTET+ using a reduced round AES block cipher as the underlying secret S-box. Extensive cryptanalysis of this algorithm allows us to claim 127 bits of security.Such tweakable enciphering schemes with huge block sizes become desirable in the context of disk encryption, since processing a whole sector as a single block significantly worsens the granularity for attackers when compared to, for example, AES-XTS, which treats every 16-byte block on the disk independently. Besides, as a huge amount of data is being stored and encrypted at rest under many different keys in clouds, beyond-birthday-bound security will most likely become necessary in the short term.
Published: 2021
Full Text: View/download PDF

27. A two-dimensional high-order well-balanced scheme for the shallow water equations with topography and Manning friction

Author: Victor Michel-Dansac, Françoise Foucher, Christophe Berthon, Stéphane Clain, TOkamaks and NUmerical Simulations (TONUS), Institut de Recherche Mathématique Avancée (IRMA), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Laboratoire de Mathématiques Jean Leray (LMJL), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-Centre National de la Recherche Scientifique (CNRS), Centro de Matemática [Minho] (CMAT), Universidade do Minho = University of Minho [Braga], Centro de Física da Universidade do Minho (CFUM), École Centrale de Nantes (ECN), FEDER – Fundo Europeu de Desenvolvimento Regional, Portugal, through COMPETE 2020 – Programa Operational Fatores de Competitividade, FCT – Fundação para a Ciência e a Tecnologia, Portugal, project No. UID/FIS/04650/2013 and project No. POCI-01-0145-FEDER-028118., ANR-19-CE46-0004,MUFFIN,Multiéchelle et Trefftz pour le transport numérique(2019), ANR-11-LABX-0020,LEBESGUE,Centre de Mathématiques Henri Lebesgue : fondements, interactions, applications et Formation(2011), Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Inria Nancy - Grand Est, Centre National de la Recherche Scientifique (CNRS)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN), Universidade do Minho, Institut de Mathématiques de Toulouse UMR5219 (IMT), Institut National des Sciences Appliquées - Toulouse (INSA Toulouse), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université Toulouse 1 Capitole (UT1), Université Fédérale Toulouse Midi-Pyrénées-Université Fédérale Toulouse Midi-Pyrénées-Université Toulouse - Jean Jaurès (UT2J)-Université Toulouse III - Paul Sabatier (UT3), Université Fédérale Toulouse Midi-Pyrénées-Centre National de la Recherche Scientifique (CNRS), Institut National des Sciences Appliquées (INSA), and Université de Nantes - Faculté des Sciences et des Techniques
Subjects: Polynomial, Steady state (electronics), General Computer Science, 010103 numerical & computational mathematics, Space (mathematics), 01 natural sciences, Simple (abstract algebra), Godunov-type schemes, FOS: Mathematics, 2010 MSC: 65M08, 65M12, Applied mathematics, [MATH.MATH-AP]Mathematics [math]/Analysis of PDEs [math.AP], Convex combination, Mathematics - Numerical Analysis, [PHYS.MECA.MEFL]Physics [physics]/Mechanics [physics]/Fluid mechanics [physics.class-ph], 0101 mathematics, Shallow water equations, Mathematics, high-order schemes, MSC: 65M08, 65M12, shallow water equations, moving steady states, Detector, General Engineering, Numerical Analysis (math.NA), 010101 applied mathematics, Scheme (mathematics), well-balanced schemes, Manning friction, [MATH.MATH-NA]Mathematics [math]/Numerical Analysis [math.NA], 65M08, 65M12
Abstract: International audience; We develop a two-dimensional high-order numerical scheme that exactly preserves and captures the moving steady states of the shallow water equations with topography or Manning friction. The high-order accuracy relies on a suitable polynomial reconstruction, while the well-balancedness property is based on the first-order scheme from [Michel-Dansac et al., 2016 & Michel-Dansac et al., 2017], extended to two space dimensions. To get both properties, we use a convex combination between the high-order scheme and the first-order well-balanced scheme. By adequately choosing the convex combination parameter following a very simple steady state detector, we ensure that the resulting scheme is both high-order accurate and well-balanced. The method is then supplemented with a MOOD procedure to eliminate the spurious oscillations coming from the high-order polynomial reconstruction and to guarantee the physical admissibility of the solution. Numerical experiments show that the scheme indeed possesses the claimed properties. The simulation of the 2011 Japan tsunami, on real data, further confirms the relevance of this technique.
Published: 2021
Full Text: View/download PDF

28. Synchronization Modulo k in Dynamic Networks

Author: Louis Penet de Monterno, Bernadette Charron-Bost, Stephan Merz, Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), École polytechnique (X)-Centre National de la Recherche Scientifique (CNRS), Département d'informatique de l'École normale supérieure (DI-ENS), École normale supérieure - Paris (ENS Paris), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Colette Johnen and Elad Michael Schiller and Stefan Schmid, Département d'informatique - ENS Paris (DI-ENS), Department of Formal Methods (LORIA - FM), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, École normale supérieure - Paris (ENS-PSL), Analyse Statique par Interprétation Abstraite (ANTIQUE), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-École normale supérieure - Paris (ENS-PSL), Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria), Proof-oriented development of computer-based systems (MOSEL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Colette Johnen, Elad Michael Schiller, and Stefan Schmid
Subjects: 03 medical and health sciences, 0302 clinical medicine, 010201 computation theory & mathematics, 030220 oncology & carcinogenesis, [INFO]Computer Science [cs], 0102 computer and information sciences, 01 natural sciences
Abstract: International audience; We define the mod k-synchronization problem as a weakening of the Firing Squad problem, where all nodes fire not at the same round, but at rounds that are all equal modulo k. We propose an algorithm that achieves mod k-synchronization in any dynamic network where there exist – possibly several – fixed spanning stars within each period of Delta consecutive rounds. In other words, we require that there always exists a temporal path of length at most Delta between some fixed node gamma and every other node. As opposed to the perfect synchronization achieved in the Firing Squad problem, mod k-synchronization thus does not require any strong connectivity property in the network. In our algorithm, all the nodes "know'' Delta, but they ignore what nodes are the centers of the spanning stars. We also prove that if the bound Delta for guaranteeing fixed spanning stars exists but is unknown to the agents, then mod k-synchronization is impossible.All nodes in our algorithm fire in less that 6kn + 4k rounds after all nodes become active, but unfortunately use unbounded counters. We then propose a refinement of this algorithm so that it becomes finite state while maintaining the same time complexity. The correctness of our first algorithm has been formally established in the proof assistant Isabelle.
Published: 2021
Full Text: View/download PDF

29. Automated Orchestration of Security Chains Driven by Process Learning

Author: Stephan Merz, Abdelkader Lahmadi, Rémi Badonnel, Nicolas Schnepf, Resilience and Elasticity for Security and ScalabiliTy of dynamic networked systems (RESIST), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Networks, Systems and Services (LORIA - NSS), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), European Project: 830927,CONCORDIA(2019), Zincir-Heywood, Nur, Diao, Yixin, and Mellia, Marco
Subjects: Exploit, Process (engineering), Computer science, business.industry, Distributed computing, 020206 networking & telecommunications, 020207 software engineering, 02 engineering and technology, Intrusion detection system, Automation, Set (abstract data type), [INFO.INFO-NI]Computer Science [cs]/Networking and Internet Architecture [cs.NI], 0202 electrical engineering, electronic engineering, information engineering, Security management, Orchestration (computing), business, Software-defined networking, ComputingMilieux_MISCELLANEOUS
Abstract: International audience; Connected devices, such as smartphones and tablets, are exposed to a large variety of attacks. Their protection is often challenged by their resource constraints in terms of CPU, memory and energy. Security chains, composed of security functions such as firewalls, intrusion detection systems and data leakage prevention mechanisms, offer new perspectives to protect these devices using software-defined networking and network function virtualization. However, the complexity and dynamics of these chains require new automation techniques to orchestrate them. This chapter describes an automated orchestration methodology for security chains in order to secure connected devices and their applications. This methodology exploits process learning to establish behavioral models and infer security constraints represented as logical predicates. It then generates and merges a set of chains of security functions on the basis of these predicates. These chains are finally compiled into low-level configuration rules and deployed into the network, optimizing for the underlying topology. The benefits and limits of such a methodology combining machine learning and verification techniques are evaluated by a set of experimental results.
Published: 2021
Full Text: View/download PDF

30. Alethe: Towards a Generic SMT Proof Format (extended abstract)

Author: Pascal Fontaine, Hans-Jörg Schurr, Haniel Barbosa, Mathias Fleury, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Proof-oriented development of computer-based systems (MOSEL), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria), Johannes Kepler University Linz [Linz] (JKU), Universidade Federal de Minas Gerais [Belo Horizonte] (UFMG), Université de Liège, European Project: 713999,H2020,Matryoshka(2017), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and Johannes Kepler Universität Linz - Johannes Kepler University Linz [Autriche] (JKU)
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, I.2.3, Computer science, Programming language, Multiple applications, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 02 engineering and technology, Mathematical proof, computer.software_genre, Logic in Computer Science (cs.LO), 03 medical and health sciences, 0302 clinical medicine, 030220 oncology & carcinogenesis, Satisfiability modulo theories, 0202 electrical engineering, electronic engineering, information engineering, computer
Abstract: The first iteration of the proof format used by the SMT solver veriT was presented ten years ago at the first PxTP workshop. Since then the format has matured. veriT proofs are used within multiple applications, and other solvers generate proofs in the same format. We would now like to gather feedback from the community to guide future developments. Towards this, we review the history of the format, present our pragmatic approach to develop the format, and also discuss problems that might arise when other solvers use the format., In Proceedings PxTP 2021, arXiv:2107.01544
Published: 2021
Full Text: View/download PDF

31. E-Cyclist: Implementation of an Efficient Validation of FOL ID Cyclic Induction Reasoning (Tool Description)

Author: Stratulat, Sorin, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), and Max-Planck-Gesellschaft-Max-Planck-Gesellschaft
Subjects: [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC], TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Abstract: International audience; Checking the soundness of cyclic induction reasoning for first-order logic with inductive definitions (FOLID) is decidable but the standard checking method is based on an exponential complement operation for Büchi automata. Recently, we introduced a polynomial checking method whose most expensive steps recall the comparisons done with multiset path orderings. We describe the implementation of our method in the Cyclist prover. Referred to as E-Cyclist, it successfully checked all the proofs included in the original distribution of Cyclist. Heuristics have been devised to automatically define, from the analysis of the proof derivations, the trace-based ordering measures that guarantee the soundness property.
Published: 2021

32. Algorithmic Reduction of Biological Networks with Multiple Time Scales

Author: Ovidiu Radulescu, Sebastian Walcher, Christoph Lüders, Thomas Sturm, Niclas Kruff, Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, ANR-17-CE40-0036,SYMBIONT,Méthodes symboliques pour les réseaux biologiques(2017), Rheinisch-Westfälische Technische Hochschule Aachen University (RWTH), Rheinische Friedrich-Wilhelms-Universität Bonn, Dynamique des interactions membranaires normales et pathologiques (DIMNP), Université Montpellier 1 (UM1)-Université Montpellier 2 - Sciences et Techniques (UM2)-Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS), Université de Montpellier (UM), Centre National de la Recherche Scientifique (CNRS), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Saarland University [Saarbrücken], Sturm, Thomas, Méthodes symboliques pour les réseaux biologiques - - SYMBIONT2017 - ANR-17-CE40-0036 - AAPG2017 - VALID, RWTH Aachen University, University of Bonn, LPHI - Laboratory of Pathogen Host Interactions (LPHI), Université de Montpellier (UM)-Centre National de la Recherche Scientifique (CNRS), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, This work has been supported by the interdisciplinary bilateral project ANR-17-CE40-0036/DFG391322026 SYMBIONT., Universität Bonn = University of Bonn, and Laboratory of Pathogen Host Interactions [Montpellier] (LPHI)
Subjects: FOS: Computer and information sciences, Computer Science - Symbolic Computation, 37D10, Computer Science - Logic in Computer Science, [INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO], Computer science, Molecular Networks (q-bio.MN), Dynamical Systems (math.DS), 92C45, 01 natural sciences, Real algebraic computation, Secondary 14P10, Symbolic computation, Satisfiability modulo theories, Logic computation, Quantitative Biology - Molecular Networks, Invariant (mathematics), Mathematics - Dynamical Systems, Singular perturbation, Invariant set, Multiple time scales, [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC], Sequence, Polynomial differential equations, Applied Mathematics, [INFO.INFO-SC] Computer Science [cs]/Symbolic Computation [cs.SC], BioModels Database, [MATH.MATH-AG] Mathematics [math]/Algebraic Geometry [math.AG], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [SDV.BBM.MN]Life Sciences [q-bio]/Biochemistry, Molecular Biology/Molecular Networks [q-bio.MN], Computational Mathematics, Computational Theory and Mathematics, 010201 computation theory & mathematics, Dimension reduction, Tropical geometry Mathematics Subject Classification Primary 68W30, Chemical reaction network, Dynamical systems theory, [MATH.MATH-DS]Mathematics [math]/Dynamical Systems [math.DS], [MATH.MATH-DS] Mathematics [math]/Dynamical Systems [math.DS], 0102 computer and information sciences, Symbolic Computation (cs.SC), FOS: Mathematics, 0101 mathematics, 010102 general mathematics, 68W30 (Primary), 14P10, 34E15, 37D10, 92C45 (Secondary), 34E15, Compartmental model, Logic in Computer Science (cs.LO), Algebra, [SDV.BBM.MN] Life Sciences [q-bio]/Biochemistry, Molecular Biology/Molecular Networks [q-bio.MN], FOS: Biological sciences, [MATH.MATH-AG]Mathematics [math]/Algebraic Geometry [math.AG], ddc:004, Biological network
Abstract: Mathematics in computer science 15(3), 499-534 (2021). doi:10.1007/s11786-021-00515-2 special issue: "Computer Algebra in Scientific Computing 2020 / Issue editors: Matthew England, Francois Boulier, Timur Sadykov, Thomas Sturm", Published by Springer International Publishing AG, Cham (ZG)
Published: 2021
Full Text: View/download PDF

33. Computer Algebra in Scientific Computing 2020

Author: England, Matthew, Boulier, François, Sadykov, Timur, Sturm, Thomas, Coventry University, University of Lille, Plekhanov Russian University of Economics [Moscow] (PRUE), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Proof-oriented development of computer-based systems (MOSEL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Universität des Saarlandes [Saarbrücken], Centre National de la Recherche Scientifique (CNRS), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and Saarland University [Saarbrücken]
Subjects: [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC], ComputingMilieux_MISCELLANEOUS
Abstract: International audience
Published: 2021

34. CFL-less Discontinuous Galerkin solver

Author: GERHARD, Pierre, HELLUY, Philippe, MICHEL-DANSAC, Victor, Institut de Recherche Mathématique Avancée (IRMA), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS), TOkamaks and NUmerical Simulations (TONUS), Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), ANR-20-ASTC-0028,M2CEM,Etude de stratégies Multi-échelles pour la simulation en Compatibilité Electromagnétique(2020), Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA), and Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Centre National de la Recherche Scientifique (CNRS)-Université de Strasbourg (UNISTRA)-Inria Nancy - Grand Est
Subjects: CFL-less, [MATH.MATH-AP]Mathematics [math]/Analysis of PDEs [math.AP], kinetic approximation, Computer Science::Numerical Analysis, [MATH.MATH-NA]Mathematics [math]/Numerical Analysis [math.NA], Mathematics::Numerical Analysis, discontinuous Galerkin
Abstract: We describe an explicit Discontinuous Galerkin (DG) kinetic scheme for solving systems of balance laws. The solver is stable for an arbitrary CFL number and has the complexity of an explicit scheme. It can be applied to any hyperbolic system of balance laws [Aregba-Driollet & Natalini, 2000; Coulette, Franck, Helluy, Mehrenberger & Navoret, 2019]. In this work, we assess the performance of the scheme in the particular case of the three-dimensional wave equation and of Maxwell’s equations. We measure the benefit of the CFL-less feature and the parallel possibilities of method.
Published: 2021

35. Politeness for the Theory of Algebraic Datatypes (Extended Abstract)

Author: Yoni Zohar, Christophe Ringeissen, Clark Barrett, Ying Sheng, Jane Lange, Pascal Fontaine, Stanford University, Proof techniques for security protocols (PESTO), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Université de Liège, Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, and Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: Computer science, Politeness, media_common.quotation_subject, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], Disjoint sets, 16. Peace & justice, Computer Science::Computers and Society, Algebra, Cover (topology), Simple (abstract algebra), Satisfiability modulo theories, Computer Science::Logic in Computer Science, Natural (music), Computer Science::Programming Languages, Automated reasoning, Algebraic number, media_common
Abstract: International audience; Algebraic datatypes, and among them lists and trees, have attracted a lot of interest in automated reasoning and Satisfiability Modulo Theories (SMT). Since its latest stable version, the SMT-LIB standard defines a theory of algebraic datatypes, which is currently supported by several mainstream SMT solvers. In this paper, we study this particular theory of datatypes and prove that it is strongly polite, showing also how it can be combined with other arbitrary disjoint theories using polite combination. Our results cover both inductive and finite datatypes, as well as their union. The combination method uses a new, simple, and natural notion of additivity, that enables deducing strong politeness from (weak) politeness.
Published: 2021
Full Text: View/download PDF

36. IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability

Author: Étienne André, Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Rustan Leino and Alexandra Silva, ANR-19-CE25-0015,ProMiS,Mitigation formelle d'attaques via canaux auxiliaires par vérification paramétrée(2019), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Model checking, Correctness, parameter synthesis, Computer science, Concurrency, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, parametric timed automata, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, model checking, Decidability, Automaton, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], real-time systems, 010201 computation theory & mathematics, Robustness (computer science), Parametric model, 0202 electrical engineering, electronic engineering, information engineering, Algorithm, Parametric statistics
Abstract: Real-time systems are notoriously hard to verify due to nondeterminism, concurrency and timing constraints. When timing constants are uncertain (in early the design phase, or due to slight variations of the timing bounds), timed model checking techniques may not be satisfactory. In contrast, parametric timed model checking synthesizes timing values ensuring correctness. takes as input an extension of parametric timed automata (PTAs), a powerful formalism to formally verify critical real-time systems. extends PTAs with multi-rate clocks, global rational-valued variables and a set of additional useful features. We describe here the new features and algorithms offered by 3, that moved along the years from a simple prototype dedicated to robustness analysis to a standalone parametric model checker for timed systems.
Published: 2021
Full Text: View/download PDF

37. Generalized Completeness for SOS Resolution and its Application to a New Notion of Relevance

Author: Fajar Haifani, Sophie Tourret, Christoph Weidenbach, Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Max Planck Institute for Informatics [Saarbrücken], Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Proof-oriented development of computer-based systems (MOSEL), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Discrete mathematics, Existential quantification, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 02 engineering and technology, Resolution (logic), 16. Peace & justice, Set (abstract data type), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, If and only if, 020204 information systems, Completeness (logic), TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Unsatisfiable core, 0202 electrical engineering, electronic engineering, information engineering, 020201 artificial intelligence & image processing, Relevance (information retrieval), Automated reasoning, Mathematics
Abstract: We prove the SOS strategy for first-order resolution to be refutationally complete on a clause setNand set-of-supportSif and only if there exists a clause inSthat occurs in a resolution refutation from$$N\cup S$$N∪S. This strictly generalizes and sharpens the original completeness result requiringNto be satisfiable. The generalized SOS completeness result supports automated reasoning on a new notion of relevance aiming at capturing the support of a clause in the refutation of a clause set. A clauseCisrelevantfor refuting a clause setNifCoccurs in every refutation ofN. The clauseCissemi-relevant, if it occurs in some refutation, i.e., if there exists an SOS refutation with set-of-support$$S = \{C\}$$S={C}from$$N\setminus \{C\}$$N\{C}. A clause that does not occur in any refutation fromNisirrelevant, i.e., it is not semi-relevant. Our new notion of relevance separates clauses in a proof that are ultimately needed from clauses that may be replaced by different clauses. In this way it provides insights towards proof explanation in refutations beyond existing notions such as that of an unsatisfiable core.
Published: 2021
Full Text: View/download PDF

38. Superposition for Full Higher-order Logic

Author: Bentkamp, A., Blanchette, J., Tourret, S., Vukmirović, P., Platzer, André, Sutcliffe, Geoff, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Computer Systems Section - Vrije Universiteit Amsterdam, Vrije Universiteit Amsterdam [Amsterdam] (VU), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Platzer, André, Sutcliffe, Geoff, Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Proof-oriented development of computer-based systems (MOSEL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Theoretical Computer Science, and Network Institute
Subjects: Semantics (computer science), [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, 16. Peace & justice, Lambda, 01 natural sciences, Higher-order logic, Superposition principle, Theorem provers, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, 010201 computation theory & mathematics, TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Extensionality, 0202 electrical engineering, electronic engineering, information engineering, Calculus, Boolean data type, Mathematics
Abstract: We recently designed two calculi as stepping stones towards superposition for full higher-order logic: Boolean-free$$\lambda $$λ-superposition and superposition for first-order logic with interpreted Booleans. Stepping on these stones, we finally reach a sound and refutationally complete calculus for higher-order logic with polymorphism, extensionality, Hilbert choice, and Henkin semantics. In addition to the complexity of combining the calculus’s two predecessors, new challenges arise from the interplay between$$\lambda $$λ-terms and Booleans. Our implementation in Zipperposition outperforms all other higher-order theorem provers and is on a par with an earlier, pragmatic prototype of Booleans in Zipperposition.
Published: 2021
Full Text: View/download PDF

39. Superposition with First-class {B}ooleans and Inprocessing Clausification

Author: Nummelin, V., Bentkamp, A., Tourret, S., Vukmirović, P., Platzer, A., Sutcliffe, G., Vrije Universiteit Amsterdam [Amsterdam] (VU), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Computer Science, Theoretical Computer Science, Network Institute, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Proof-oriented development of computer-based systems (MOSEL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Platzer, A., and Sutcliffe, G.
Subjects: Computer science, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 02 engineering and technology, 16. Peace & justice, First class, [INFO.INFO-AI]Computer Science [cs]/Artificial Intelligence [cs.AI], Superposition principle, Automated theorem proving, TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Encoding (memory), TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Computer Science::Logic in Computer Science, Superposition calculus, 0202 electrical engineering, electronic engineering, information engineering, Calculus, Preprocessor, 020201 artificial intelligence & image processing, Boolean data type, Axiom
Abstract: We present a complete superposition calculus for first-order logic with an interpreted Boolean type. Our motivation is to lay the foundation for refutationally complete calculi in more expressive logics with Booleans, such as higher-order logic, and to make superposition work efficiently on problems that would be obfuscated when using clausification as preprocessing. Working directly on formulas, our calculus avoids the costly axiomatic encoding of the theory of Booleans into first-order logic and offers various ways to interleave clausification with other derivation steps. We evaluate our calculus using the Zipperposition theorem prover, and observe that, with no tuning of parameters, our approach is on a par with the state-of-the-art approach.
Published: 2021
Full Text: View/download PDF

40. Representing infinite hyperbolic periodic Delaunay triangulations using finitely many Dirichlet domains

Author: Despré, Vincent, Kolbe, Benedikt, Teillaud, Monique, Geometric Algorithms and Models Beyond the Linear and Euclidean realm (GAMBLE ), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), The authors were supported by grant ANR-17-CE40-0033 of the French National Research Agency ANR (project SoS)(https://members.loria.fr/Monique.Teillaud/collab/SoS/)., ANR-17-CE40-0033,SoS,Structures sur des surfaces(2017), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Kolbe, Benedikt, Structures sur des surfaces - - SoS2017 - ANR-17-CE40-0033 - AAPG2017 - VALID, Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, and Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: Hyperbolic surfaces, Fuchsian group, [INFO.INFO-CG] Computer Science [cs]/Computational Geometry [cs.CG], Delaunay triangulations, [MATH.MATH-GT]Mathematics [math]/Geometric Topology [math.GT], Computer Science::Computational Geometry, Dirichlet domain, [INFO.INFO-CG]Computer Science [cs]/Computational Geometry [cs.CG], Topology, [MATH.MATH-GT] Mathematics [math]/Geometric Topology [math.GT]
Abstract: Version 2: Restructuring of the text, with focus on the essential results. Simplification of some of the proofs; The Delaunay triangulation of a set of points $P$ on a hyperbolicsurface is the projection of the Delaunay triangulation of the set$\tilde{P}$ of lifted points in the hyperbolic plane. Since$\tilde{P}$ is infinite, the algorithms to compute Delaunaytriangulations in the plane do not generalize naturally. Assuming thatthe surface comes with a Dirichlet domain, we exhibit a finite set of points that captures the full triangulation.Indeed, we prove that an edge of a Delaunay triangulation has acombinatorial length (a notion we define in the paper) smaller than$12g-6$ with respect to a Dirichlet domain. On the way, we prove thatboth the edges of a Delaunay triangulation and of a Dirichlet domainhave some kind of distance minimizing properties that are of intrinsicinterest.The bounds produced in this paper depend only on the topology of thesurface. They provide mathematical foundations for hyperbolic analogsof the algorithms to compute periodic Delaunay triangulations inEuclidean space.
Published: 2021

41. Informational Texture Synthesis

Author: Lefebvre, Sylvain, Wei, Li-Yi, Barnes, Connelly, Matter from Graphics (MFX), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Adobe Research, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Geometry and Lighting (ALICE), Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, and Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: Hardware_REGISTER-TRANSFER-LEVELIMPLEMENTATION, [INFO.INFO-GR]Computer Science [cs]/Graphics [cs.GR]
Abstract: This paper presents a novel technique to embed messages into textures synthesized from tiles with boundary constraints. The messages are encoded in the choices that the synthesis algorithm normally makes at random during the synthesis process. Images embedding messages are not distinguishable from images that are not embedding any message. The random sequence seed used during synthesis can act as a password.
Published: 2021

42. Efficient Methods to Search for Best Differential Characteristics on SKINNY

Author: Charles Prud'homme, Paul Huynh, Victor Mollimard, Stéphanie Delaune, Patrick Derbez, Marine Minier, Embedded Security and Cryptography / Sécurité cryptographie embarquée (EMSEC), SYSTÈMES LARGE ÉCHELLE (IRISA-D1), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), Security & PrIvaCY (SPICY), Cryptology, arithmetic : algebraic methods for better algorithms (CARAMBA), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Théorie, Algorithmes et Systèmes en Contraintes (LS2N - équipe TASC ), Laboratoire des Sciences du Numérique de Nantes (LS2N), Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Nantes - UFR des Sciences et des Techniques (UN UFR ST), Département Automatique, Productique et Informatique (IMT Atlantique - DAPI), IMT Atlantique (IMT Atlantique), The research leading to these results has received funding from the French National Research Agency (ANR) under the project Decrypt ANR-18-CE39-0007., Kazue Sako, Nils Ole Tippenhauer, ANR-18-CE39-0007,DeCrypt,Langage Déclaratif pour la cryptographie symétrique(2018), Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Théorie, Algorithmes et Systèmes en Contraintes (TASC ), Université de Nantes (UN)-Université de Nantes (UN)-École Centrale de Nantes (ECN)-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT), Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, and Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: Differential cryptanalysis, Computer science, 020206 networking & telecommunications, Data_CODINGANDINFORMATIONTHEORY, 0102 computer and information sciences, 02 engineering and technology, 01 natural sciences, SKINNY, 010201 computation theory & mathematics, tools, 0202 electrical engineering, electronic engineering, information engineering, [INFO]Computer Science [cs], Algorithm, Differential (mathematics), differential cryptanalysis, automatic tools
Abstract: International audience; Evaluating resistance of ciphers against differential cryptanalysis is essential to define the number of rounds of new designs and to mount attacks derived from differential cryptanalysis. In this paper, we propose automatic tools to find the best differential characteristics on the SKINNY block cipher. As usually done in the literature, we split this search in two stages denoted by Step 1 and Step 2. In Step 1, we aim at finding all truncated differential characteristics with a low enough number of active Sboxes. Then, in Step 2, we try to instantiate each difference value while maximizing the overall differential characteristic probability. We solve Step 1 using an ad-hoc method inspired from the work of Fouque et al. whereas Step 2 is modelized for the Choco-solver library as it seems to outperform all previous methods on this stage. Notably, for SKINNY-128 in the SK model and for 13 rounds, we retrieve the results of Abdelkhalek et al. within a few seconds (to compare with 16 days) and we provide, for the first time, the best differential related-tweakey characteristics up to 14 rounds for the TK1 model. Regarding the TK2 and the TK3 models, we were not able to test all the solutions Step 1, and thus the differential characteristics we found up to 16 and 17 rounds are not necessarily optimal.
Published: 2021
Full Text: View/download PDF

43. A Refinement Strategy for Hybrid System Design with Safety Constraints

Author: Zheng Cheng, Dominique Méry, Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria), Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, TELECOM Nancy, Université de Lorraine (UL), ANR-17-CE25-0005,DISCONT,Intégration correcte de modèles discrets et continus(2017), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), ANR, Université de Lorraine, INRIA, CNRS, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Computer science, Event (computing), Distributed computing, Control (management), formal modelling, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 0102 computer and information sciences, 02 engineering and technology, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], Safety constraints, hybrid systems, 01 natural sciences, Continuous variable, Heating system, [INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL], 010201 computation theory & mathematics, Hybrid system, Discrete Modeling, 0202 electrical engineering, electronic engineering, information engineering, Event-B, patterns, continuous variables
Abstract: International audience; Whenever continuous dynamics and discrete control interact, hybrid systems arise. As hybrid systems become ubiquitous and more and more complex, analysis and synthesis techniques are in high demand to design safe hybrid systems. This is however challenging due to the nature of hybrid systems and their designs, and the question of how to formulate and reason their safety problems. Previous work has demonstrated how to extend the discrete modeling language Event-B with continuous support to integrate traditional refinement in hybrid system design. In the same spirit, we extend previous work by proposing a strategy that can coherently refine an abstract hybrid system design with safety constraints down to a concrete one, integrated with implementable discrete control, that can behave safely. We demonstrate our proposal on a smart heating system that regulates room temperature between two references, and we share our experience.
Published: 2021
Full Text: View/download PDF

44. Restricted Power Diagrams on the GPU

Author: Bruno Levy, Nicolas Ray, Dmitry Sokolov, Justine Basselin, Laurent Alonso, Sylvain Lefebvre, Structurer des formes géométriques (PIXEL), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Matter from Graphics (MFX), Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)
Subjects: Speedup, Voronoi Diagram, Computer science, [INFO.INFO-DS]Computer Science [cs]/Data Structures and Algorithms [cs.DS], Parallel algorithm, Triangulation (social science), 020207 software engineering, 010103 numerical & computational mathematics, 02 engineering and technology, Computational geometry, [INFO.INFO-CG]Computer Science [cs]/Computational Geometry [cs.CG], 01 natural sciences, Computer Graphics and Computer-Aided Design, Computational science, Domain (software engineering), Power Diagram, 0202 electrical engineering, electronic engineering, information engineering, Power diagram, 0101 mathematics, General-purpose computing on graphics processing units, [INFO.INFO-DC]Computer Science [cs]/Distributed, Parallel, and Cluster Computing [cs.DC], Voronoi diagram, GPU Programming
Abstract: International audience; We propose a method to simultaneously decompose a 3D object into power diagram cells and to integrate given functions in each of the obtained simple regions. We offer a novel, highly parallel algorithm that lends itself to an efficient GPU implementation. It is optimized for algorithms that need to compute many decompositions, for instance, centroidal Voronoi tesselation algorithms and incompressible fluid dynamics simulations. We propose an efficient solution that directly evaluates the integrals over every cell without computing the power diagram explicitly and without intersecting it with a tetrahedralization of the domain. Most computations are performed on the fly, without storing the power diagram. We manipulate a triangulation of the boundary of the domain (instead of tetrahedralizing the domain) to speed up the process. Moreover, the cells are treated independently one from another, making it possible to trivially scale up on a parallel architecture. Despite recent Voronoi diagram generation methods optimized for the GPU, computing integrals over restricted power diagrams still poses significant challenges; the restriction to a complex simulation domain is difficult and likely to be slow. It is not trivial to determine when a cell of a power diagram is completely computed, and the resulting integrals (e.g. the weighted Laplacian operator matrix) do not fit into fast (shared) GPU memory. We address all these issues and boost the performance of the state-of-the-art algorithms by a factor 2 to 3 for (unrestricted) Voronoi diagrams and a ×50 speed-up with respect to CPU implementations for restricted power diagrams. An essential ingredient to achieve this is our new scheduling strategy that allows us to treat each Voronoi/power diagram cell with optimal settings and to benefit from the fast memory.
Published: 2021
Full Text: View/download PDF

45. Foreword, with a Dedication to {Andreas Weber}

Author: Matthew England, Thomas Sturm, Werner M. Seiler, Timur Sadykov, Wolfram Koepf, Coventry University, Universität Kassel [Kassel], Plekhanov Russian University of Economics [Moscow] (PRUE), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Proof-oriented development of computer-based systems (MOSEL), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Universität des Saarlandes [Saarbrücken], ANR-17-CE40-0036,SYMBIONT,Méthodes symboliques pour les réseaux biologiques(2017), Centre National de la Recherche Scientifique (CNRS), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and Saarland University [Saarbrücken]
Subjects: [INFO.INFO-SC]Computer Science [cs]/Symbolic Computation [cs.SC], Applied Mathematics, 010102 general mathematics, [MATH.MATH-DS]Mathematics [math]/Dynamical Systems [math.DS], [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], [SDV.BBM.MN]Life Sciences [q-bio]/Biochemistry, Molecular Biology/Molecular Networks [q-bio.MN], 0102 computer and information sciences, 01 natural sciences, Computational Mathematics, Computational Theory and Mathematics, 010201 computation theory & mathematics, [MATH.MATH-AG]Mathematics [math]/Algebraic Geometry [math.AG], 0101 mathematics, ComputingMilieux_MISCELLANEOUS
Abstract: International audience
Published: 2021
Full Text: View/download PDF

46. TLA+ model checking made symbolic

Author: Igor Konnov, Thanh-Hai Tran, Jure Kukovec, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Proof-oriented development of computer-based systems (MOSEL), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Vienna University of Technology (TU Wien), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), and Max-Planck-Gesellschaft-Max-Planck-Gesellschaft
Subjects: Model checking, Exploit, Relation (database), Computer science, Programming language, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE], 02 engineering and technology, computer.software_genre, Language primitive, TLA+, SMT, 020204 information systems, Formal specification, 0202 electrical engineering, electronic engineering, information engineering, State (computer science), Tuple, Safety, Risk, Reliability and Quality, Boolean data type, computer, Software
Abstract: TLA+ is a language for formal specification of all kinds of computer systems. System designers use this language to specify concurrent, distributed, and fault-tolerant protocols, which are traditionally presented in pseudo-code. TLA+ is extremely concise yet expressive: The language primitives include Booleans, integers, functions, tuples, records, sequences, and sets thereof, which can be also nested. This is probably why the only model checker for TLA+ (called TLC) relies on explicit enumeration of values and states. In this paper, we present APALACHE -- a first symbolic model checker for TLA+. Like TLC, it assumes that all specification parameters are fixed and all states are finite structures. Unlike TLC, APALACHE translates the underlying transition relation into quantifier-free SMT constraints, which allows us to exploit the power of SMT solvers. Designing this translation is the central challenge that we address in this paper. Our experiments show that APALACHE outperforms TLC on examples with large state spaces.
Published: 2019
Full Text: View/download PDF

47. Ribbed Support Vaults for 3D Printing of Hollowed Objects

Author: Thibault Tricard, Frédéric Claux, Sylvain Lefebvre, Synthèse et analyse d'images (XLIM-ASALI), XLIM (XLIM), Université de Limoges (UNILIM)-Centre National de la Recherche Scientifique (CNRS)-Université de Limoges (UNILIM)-Centre National de la Recherche Scientifique (CNRS), Matter from Graphics (MFX), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, and Institut National de Recherche en Informatique et en Automatique (Inria)
Subjects: 0209 industrial biotechnology, Fabrication, Computer science, business.industry, Process (computing), Mechanical engineering, 3D printing, 020207 software engineering, Fused filament fabrication, Context (language use), 02 engineering and technology, support structures, [INFO.INFO-CG]Computer Science [cs]/Computational Geometry [cs.CG], Object (computer science), Computer Graphics and Computer-Aided Design, 020901 industrial engineering & automation, 0202 electrical engineering, electronic engineering, information engineering, Point (geometry), Layer (object-oriented design), business, additive manufacturing, ComputingMilieux_MISCELLANEOUS
Abstract: Additive manufacturing techniques form an object by accumulating layers of material on top of one another. Each layer has to be supported by the one below for the fabrication process to succeed. To reduce print time and material usage, especially in the context of prototyping, it is often desirable to fabricate hollow objects. This exacerbates the requirement of support between consecutive layers: standard hollowing produces surfaces in overhang that cannot be directly fabricated anymore. Therefore, these surfaces require internal support structures. These are similar to external supports for overhangs, with the key difference that internal supports remain invisible within the object after fabrication. A fundamental challenge is to generate structures that provide a dense support while using little material. In this paper, we propose a novel type of support inspired by rib structures. Our approach guarantees that any point in a layer is supported by a point below, within a given threshold distance. Despite providing strong guarantees for printability, our supports remain lightweight and reliable to print. We propose a greedy support generation algorithm that creates compact hierarchies of rib-like walls. The walls are progressively eroded away and straightened, eventually merging with the interior object walls. We demonstrate our technique on a variety of models and provide performance figures in the context of Fused Filament Fabrication (FFF) 3D printing.
Published: 2019
Full Text: View/download PDF

48. Superposition with lambdas

Author: Bentkamp, Alexander, Blanchette, Jasmin, Tourret, Sophie, Vukmirović, Petar, Waldmann, Uwe, Fontaine, Pascal, Theoretical Computer Science, Network Institute, Fontaine, Pascal, Vrije Universiteit Amsterdam [Amsterdam] (VU), Computer Systems Section - Vrije Universiteit Amsterdam, Modeling and Verification of Distributed Algorithms and Systems (VERIDIS), Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Formal Methods (LORIA - FM), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Max-Planck-Gesellschaft, Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Department of Formal Methods (LORIA - FM), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft-Max-Planck-Gesellschaft, Proof-oriented development of computer-based systems (MOSEL), and Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)
Subjects: FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Logic in computer science, Unification, Computer Science - Artificial Intelligence, 02 engineering and technology, 0102 computer and information sciences, Gas meter prover, 01 natural sciences, Higher-order logic, Anonymous function, Refutational completeness, Fragment (logic), F.4.1, I.2.3, Artificial Intelligence, Computer Science::Logic in Computer Science, Superposition calculus, 0202 electrical engineering, electronic engineering, information engineering, 0101 mathematics, Rule of inference, Mathematics, Discrete mathematics, 010102 general mathematics, [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO], 020207 software engineering, 16. Peace & justice, Logic in Computer Science (cs.LO), Artificial Intelligence (cs.AI), TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES, Computational Theory and Mathematics, 010201 computation theory & mathematics, Completeness (logic), TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS, Software
Abstract: We designed a superposition calculus for a clausal fragment of extensional polymorphic higher-order logic that includes anonymous functions but excludes Booleans. The inference rules work on $$\beta \eta $$ β η -equivalence classes of $$\lambda $$ λ -terms and rely on higher-order unification to achieve refutational completeness. We implemented the calculus in the Zipperposition prover and evaluated it on TPTP and Isabelle benchmarks. The results suggest that superposition is a suitable basis for higher-order reasoning.
Published: 2019
Full Text: View/download PDF

49. Cryptanalyses de logarithmes discrets : crible algébrique et réseaux pour canaux auxiliaires

Author: de Micheli, Gabrielle, Cryptology, arithmetic : algebraic methods for better algorithms (CARAMBA), Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria), Université de Lorraine, Pierrick Gaudry, Cécile Pierrot, Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), and UL, Thèses
Subjects: Cryptanalysis, [INFO.INFO-CR]Computer Science [cs]/Cryptography and Security [cs.CR], Discrete logarithm, Logarithme discret, Attaques par canaux cachés, [INFO]Computer Science [cs], Lattices, Side-channel attacks, [INFO] Computer Science [cs], Réseaux, Cryptanalyse, [INFO.INFO-CR] Computer Science [cs]/Cryptography and Security [cs.CR]
Abstract: Public-key cryptosystems are constructed using one-way functions which ensure both the security and the efficiency of the schemes. One of the two main candidates originally considered to construct public-key cryptosystems is modular exponentiation with its hard inverse operation, computing discrete logarithms. In this thesis, we study the security of protocols that make use of modular exponentiation where the exponent is a secret of the protocol. To assess the security of such protocols, one can either estimate the hardness of directly solving the discrete logarithm problem (DLP) in the groups considered by the protocols or look at implementation vulnerabilities from fast exponentiation algorithms. One way of estimating the security of protocols based on the hardness of the discrete logarithm problem is to directly study the complexity of the algorithms that solve the latter. In this thesis, we first study the asymptotic complexity of algorithms that solve DLP over finite fields “\F_{p^n}” precisely of the form where pairings take their values. These algorithms come from the index-calculus family from which the Number Field Sieve (NFS) is an example. This study allows us to draw conclusions on the security of pairing-based protocols. We also propose a first implementation of the variant Tower Number Field Sieve (TNFS) of NFS, which has better asymptotic complexity, along with a record computation of a discrete logarithm in a 521-bit finite field with TNFS. This variant had never been implemented before due to the difficulty of sieving in higher dimensions, i.e., dimensions greater than two. Finally, the security of deployed protocols not only relies on the hardness of the underlying mathematical problem but also on the implementation of the algorithms involved. Many fast modular exponentiation algorithms have piled up over the years and some implementations have brought vulnerabilities that are exploitable by side-channel attacks, in particular cache attacks. The second aspect of this thesis thus considers key recover methods when partial information is recovered from a side channel., Les cryptosystèmes dits à clé publique sont construits à l'aide de fonctions à sens unique qui assurent à la fois la sécurité et l'efficacité des cryptosystèmes. L'un des deux principaux candidats envisagés à l'origine pour construire de tels cryptosystèmes est l'exponentiation modulaire avec son opération inverse, le calcul de logarithmes discrets. Dans cette thèse, nous étudions la sécurité de protocoles qui utilisent des exponentiations modulaires où l'exposant est un secret du protocole. Afin d'évaluer la sécurité de tels protocoles, on peut d'une part estimer la difficulté de résoudre directement le problème du logarithme discret (DLP) dans les groupes considérés par les protocoles, ou examiner les vulnérabilités issues de l'implémentation des algorithmes d'exponentiation rapide. Une première façon d'estimer la sécurité des protocoles basés sur la difficulté du problème du logarithme discret est d'étudier directement la complexité des algorithmes qui résolvent ce dernier. Dans cette thèse, nous étudions la complexité asymptotique des algorithmes qui résolvent le DLP sur des corps finis « \F_{p^n} » précisément de la forme où les couplages prennent leurs valeurs. Nous proposons également une première implémentation et un calcul record d'un logarithme discret dans un corps fini de 521 bits en utilisant l'algorithme Tower Number Field Sieve, une variante de NFS dont la complexité asymptotique est meilleure. Cette variante n'avait jamais été implémentée auparavant en raison de la difficulté du crible algébrique dans des dimensions supérieures à deux. Enfin, la sécurité des protocoles déployés ne repose pas seulement sur la difficulté du problème mathématique sous-jacent, mais aussi sur l'implémentation des algorithmes considérés. De nombreux algorithmes d'exponentiation modulaire rapide se sont accumulés au fil des ans et certaines implémentations ont fait apparaître des vulnérabilités exploitables par des attaques par canaux auxiliaires. Un second aspect de cette thèse considère donc les principales méthodes pour reconstituer une clé secrète lorsque des informations partielles sont récupérées à partir d'un canal auxiliaire.
Published: 2021

50. Isolating the Singularities of the Plane Projection of Generic Space Curves and Applications in Robotics

Author: Krait, George, Geometric Algorithms and Models Beyond the Linear and Euclidean realm (GAMBLE ), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Department of Algorithms, Computation, Image and Geometry (LORIA - ALGO), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Université de Lorraine (Nancy), Sylvain Lazard (INRIA Nancy Grand Est, Loria), Guillaume Moroz (INRIA Nancy Grand Est, Loria), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL), Université de Lorraine, Sylvain Lazard, and Guillaume Moroz
Subjects: Interval Arithmetic, Algorithmes Numériques Certifiés, Singular Curve Topology, Singularités Génériques, Topologie de Courbe Singulière, Transversality, Transversalité, Certified Numerical Algorithms, [INFO.INFO-NA]Computer Science [cs]/Numerical Analysis [cs.NA], Arithmétique d'Intervalles, [INFO.INFO-CG]Computer Science [cs]/Computational Geometry [cs.CG], Generic Singularities
Abstract: Isolating the singularities of a plane curve is the first step towards computing its topology. For this, numerical methods are efficient but not certified in general. We are interested in developing certified numerical algorithms for isolating the singularities. In order to do so, we restrict our attention to the special case of plane curves that are projections of smooth curves in higher dimensions. This type of curves appears naturally in robotics applications and scientific visualization. In this setting, we show that the singularities can be encoded by a regular square system whose solutions can be isolated with certified numerical methods. Our analysis is conditioned by assumptions that we prove to be generic using transversality theory. We also provide a semi-algorithm to check their validity. Finally, we present experiments in visualization and robotics, some of which are not reachable by other methods, and discuss the efficiency of our method.; L’isolation des points singuliers d'une courbe plane est la première étape vers le calcul de sa topologie. Pour cela, les méthodes numériques sont efficaces mais non certifiées en général. Nous sommes intéressés par le développement d'algorithmes numériques certifiés pour isoler les singularités. Pour ce faire, nous limitons notre attention au cas particulier des courbes planes qui sont des projections de courbes lisses en dimensions superieures. Ce type de courbes apparaît naturellement dans les applications robotiques et la visualisation scientifique. Dans ce cadre, nous montrons que les singularités peuvent être encodées par un système carré et régulier dont les solutions peuvent être isolées avec des méthodes numériques certifiées. Notre analyse est conditionnée par des hypothèses que nous démontrons comme étant génériques en utilisant la théorie de la transversalité; nous fournissons également un semi-algorithme pour vérifier leur validité. Enfin, nous présentons des expériences de visualisation et de robotique, dont certaines ne sont pas accessibles par d'autres méthodes, et discutons de l'efficacité de notre méthode.
Published: 2021

Catalog

Books, media, physical & digital resources

See catalog results

Searchworks

Select search scope, currently: Articles Catalog books, media & more in Jio Institute collections Articles journal articles & other e-resources

Search

Search Constraints

Refine your results

Search Limiters

Topic

Publication Year Range

Language

Publication Type

Journal

Database

Publisher

7,064 results on '"Inria Nancy - Grand Est"'

Search Results

Catalog

Select search scope, currently: Articles

Catalog

books, media & more in Jio Institute collections

Articles

journal articles & other e-resources