Search

International audience; We present new parallel explicit emptiness checks for LTL model checking. Unlike existing parallel emptiness checks, these are based on a Strongly Connected Component (SCC) enumeration, support generalized Büchi acceptance, and require no synchronization points nor recomputing procedures. A salient feature of our algorithms is the use of a global union-find data structure in which multiple threads share structural information about the automaton checked. Besides these basic algorithms, we present one architectural variant isolating threads that write to the union-find, and one extension that decomposes the automaton based on the strength of its SCCs to use more optimized emptiness checks. The results from an extensive experimentation of our algorithms and their variations show encouraging performances, especially when the decomposition technique is used.

International audience; Over the last few years, several works have proposed deep learning architectures to learn dynamical systems from observation data with no or little knowledge of the underlying physics. A line of work relies on learning representations where the dynamics of the underlying phenomenon can be described by a linear operator, based on the Koopman operator theory. However, despite being able to provide reliable long-term predictions for some dynamical systems in ideal situations, the methods proposed so far have limitations, such as requiring to discretize intrinsically continuous dynamical systems, leading to data loss, especially when handling incomplete or sparsely sampled data. Here, we propose a new deep Koopman framework that represents dynamics in an intrinsically continuous way, leading to better performance on limited training data, as exemplified on several datasets arising from dynamical systems.

International audience; Many methods relying on the morphological notion of shapes, (i.e., connected components of level sets) have been proved to be very useful for pattern analysis and recognition. Selecting meaningful level lines (boundaries of level sets) yields to simplify images while preserving salient structures. Many image simplification and/or segmentation methods are driven by the optimization of an energy functional, for instance the Mumford-Shah functional. In this article, we propose an efficient shape-based morphological filtering that very quickly compute to a locally (subordinated to the tree of shapes) optimal solution of the piecewise-constant Mumford- Shah functional. Experimental results demonstrate the efficiency, usefulness, and robustness of our method, when applied to image simplification, pre-segmentation, and detection of affine regions with viewpoint changes.

International audience; Connected filtering is a popular strategy that relies on tree-based image representations: for example, one can compute an attribute on each node of the tree and keep only the nodes for which the attribute is sufficiently strong. This operation can be seen as a thresholding of the tree, seen as a graph whose nodes are weighted by the attribute. Rather than being satisfied with a mere thresholding, we propose to expand on this idea, and to apply connected filters on this latest graph. Consequently, the filtering is done not in the space of the image, but on the space of shapes built from the image. Such a processing, that we called shape-based morphology, is a generalization of the existing tree-based connected operators. In this paper, two different applications are studied: in the first one, we apply our framework to blood vessels segmentation in retinal images. In the second one, we propose an extension of constrained connectivity. In both cases, quantitative evaluations demonstrate that shape-based filtering, a mere filtering step that we compare to more evolved processings, achieves state-of-the-art results.

The Skolem problem is a long-standing open problem in linear dynamical systems: can a linear recurrence sequence (LRS) ever reach 0 from a given initial configuration? Similarly, the positivity problem asks whether the LRS stays positive from an initial configuration. Deciding Skolem (or positivity) has been open for half a century: The best known decidability results are for LRS with special properties (e.g., low order recurrences). On the other hand, these problems are much easier for "uninitialized" variants, where the initial configuration is not fixed but can vary arbitrarily: checking if there is an initial configuration from which the LRS stays positive can be decided by polynomial time algorithms (Tiwari in 2004, Braverman in 2006). In this paper, we consider problems that lie between the initialized and uninitialized variant. More precisely, we ask if 0 (resp. negative numbers) can be avoided from every initial configuration in a neighborhood of a given initial configuration. This can be considered as a robust variant of the Skolem (resp. positivity) problem. We show that these problems lie at the frontier of decidability: if the neighborhood is given as part of the input, then robust Skolem and robust positivity are Diophantine-hard, i.e., solving either would entail major breakthrough in Diophantine approximations, as happens for (non-robust) positivity. Interestingly, this is the first Diophantine-hardness result on a variant of the Skolem problem, to the best of our knowledge. On the other hand, if one asks whether such a neighborhood exists, then the problems turn out to be decidable in their full generality, with PSPACE complexity. Our analysis is based on the set of initial configurations such that positivity holds, which leads to new insights into these difficult problems, and interesting geometrical interpretations., LIPIcs, Vol. 219, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022), pages 5:1-5:20

International audience; Among the different flavors of well-compo-sednesses on cubical grids, two of them, called respectively digital well-composedness (DWCness) and well-composedness in the sense of Alexandrov (AWCness), are known to be equivalent in 2D and in 3D. The former means that a cubical set does not contain critical configurations when the latter means that the boundary of a cubical set is made of a disjoint union of discrete surfaces. In this paper, we prove that this equivalence holds in n-D, which is of interest because today images are not only 2D or 3D but also 4D and beyond. The main benefit of this proof is that the topological properties available for AWC sets, mainly their separation properties, are also true for DWC sets, and the properties of DWC sets are also true for AWC sets: an Euler number locally computable, equivalent con-nectivities from a local or global point of view... This result is also true for gray-level images thanks to cross-section topology, which means that the sets of shapes of DWC gray-level images make a tree like the ones of AWC gray-level images.

International audience; AGAT is a Java library dedicated to the construction,handling and evaluation of binary partition trees, a hierarchical data structure providing multiscale partitioning of images and, more generally, of valued graphs.On the one hand, this library offers functionalities to build binary partition trees in the usual way, but also to define multifeature trees, a novel and richer paradigm of binary partition trees built from multiple images and / or several criteria.On the other hand, it also allows one to manipulate the binary partition trees, for instance by defining / computing tree cuts that can be interpreted in particular as segmentations when dealing with image modeling.In addition, some evaluation tools are also provided, which allow one to evaluate the quality of different binary partition trees for such segmentation tasks.AGAT can be easily handled by various kinds of users (students, researchers, practitioners).It can be used as is for experimental purposes, but can also form a basis for the development of new methods and paradigms for construction, use and intensive evaluation of binary partition trees.Beyond the usual imaging applications, its underlying structure also allows for more general developments in graph-based analysis, leading to a wide range of potential applications in computer vision, image / data analysis and machine learning.

International audience; Most contemporary supervised image segmentation methods do not preserve the initial topology of the given input (like the closeness of the contours). One can generally remark that edge points have been inserted or removed when the binary prediction and the ground truth are compared. This can be critical when accurate localization of multiple interconnected objects is required. In this paper, we present a new loss function, called, Boundary-Aware loss (BALoss), based on the Minimum Barrier Distance (MBD) cut algorithm. It is able to locate what we call the leakage pixels and to encode the boundary information coming from the given ground truth. Thanks to this adapted loss, we are able to significantly refine the quality of the predicted boundaries during the learning procedure. Furthermore, our loss function is differentiable and can be applied to any kind of neural network used in image processing. We apply this loss function on the standard U-Net and DC U-Net on Electron Microscopy datasets. They are well-known to be challenging due to their high noise level and to the close or even connected objects covering the image space. Our segmentation performance, in terms of Variation of Information (VOI) and Adapted Rank Index (ARI), are very promising and lead to ∼15% better scores of VOI and ∼5% better scores of ARI than the state-of-the-art.

International audience; Maps have been a unique source of knowledge for centuries. Such historical documents provide invaluable information for analyzing the complex spatial transformation of landscapes over important time frames. This is particularly true for urban areas that encompass multiple interleaved research domains (social sciences, economy, etc.). The large amount and significant diversity of map sources call for automatic image processing techniques in order to extract the relevant objects under a vectorial shape. The complexity of maps (text, noise, digiti-zation artifacts, etc.) has hindered the capacity of proposing a versatile and efficient raster-to-vector approaches for decades. We propose alearnable, reproducible, and reusable solution for the automatic transformation of raster maps into vector objects (building blocks, streets,rivers). It is built upon the complementary strength of mathematical morphology and convolutional neural networks through efficient edge filtering. Even more, we modify ConnNet and combine with deep edgefiltering architecture to make use of pixel connectivity information and built an end-to-end system without requiring any post-processing techniques. In this paper, we focus on the comprehensive benchmark on various architectures on multiple datasets coupled with a novel vectorization step. Our experimental results on a new public dataset using COCO Panoptic metric exhibit very encouraging results confirmedby a qualitative analysis of the success and failure cases of our approach. Code, dataset, results and extra illustrations are freely available at https://github.com/soduco/ICDAR-2021-Vectorization

International audience; Hierarchical data representations are powerful tools to analyze images and have found numerous applications in image processing. When it comes to multimodal images however, the fusion of multiple hierarchies remains an open question. Recently, the concept of braids of partitions has been proposed as a theoretical tool and possible solution to this issue. In this paper, we demonstrate the relevance of the braid structure for the hierarchical representation of multimodal images. We first propose a fully operable procedure to build a braid of partitions from two hierarchical representations. We then derive a framework for multimodal image segmentation, relying on an energetic minimization scheme conducted on the braid structure. The proposed approach is investigated on different multimodal images scenarios, and the obtained results confirm its ability to efficiently handle the multimodal information to produce more accurate segmentation outputs.

International audience; We introduce the Software Heritage filesystem (SwhFS), a user-space filesystem that integrates large-scale open source software archival with development workflows. SwhFS provides a POSIX filesystem view of Software Heritage, the largest public archive of software source code and version control system (VCS) development history.Using SwhFS, developers can quickly "checkout" any of the 2 billion commits archived by Software Heritage, even after they disappear from their previous known location and without incurring the performance cost of repository cloning. SwhFS works across unrelated repositories and different VCS technologies. Other source code artifacts archived by Software Heritage-individual source code files and trees, releases, and branches-can also be accessed using common programming tools and custom scripts, as if they were locally available.A screencast of SwhFS is available online at dx.doi.org/10.5281/zenodo.4531411.

Supplementary material (code, extra figures) available at https://github.com/soduco/paper-dgmm2021/; International audience; The digitization of historical maps enables the study of ancient, fragile, unique, and hardly accessible information sources. Main map features can be retrieved and tracked through the time for subsequent thematic analysis. The goal of this work is the vectorization step, i.e., the extraction of vector shapes of the objects of interest from raster images of maps. We are particularly interested in closed shape detection such as buildings, building blocks, gardens, rivers, etc. in order to monitor their temporal evolution. Historical map images present significant pattern recognition challenges. The extraction of closed shapes by using traditional Mathematical Morphology (MM) is highly challenging due to the overlapping of multiple map features and texts. Moreover, state-of-the-art Convolutional Neural Networks (CNN) are perfectly designed for content image filtering but provide no guarantee about closed shape detection. Also, the lack of textural and color information of historical maps makes it hard for CNN to detect shapes that are represented by only their boundaries. Our contribution is a pipeline that combines the strengths of CNN (efficient edge detection and filtering) and MM (guaranteed extraction of closed shapes) in order to achieve such a task. The evaluation of our approach on a public dataset shows its effectiveness for extracting the closed boundaries of objects in historical maps.

International audience; Quicklisp is a library manager working with your existing Common Lisp implementation to download and install around 2000 libraries, from a central archive. Quickref, an application itself written in Common Lisp, generates, automatically and by introspection, a technical documentation for every library in Quicklisp, and produces a website for this documentation. In this paper, we present a corpus processing and analysis pipeline for Quickref. This pipeline consists of a set of natural language processing blocks allowing us to analyze Quicklisp libraries, based on natural language contents sources such as README files, docstrings, or symbol names. The ultimate purpose of this pipeline is the generation of a keyword index for Quickref, although other applications such as word clouds or topic analysis are also envisioned. CCS CONCEPTS • Information systems → Information extraction; Retrieval effectiveness; Presentation of retrieval results; • Software and its engineering → Software libraries and repositories.

The Endoscopy Computer Vision Challenge (EndoCV) is a crowd-sourcing initiative to address eminent problems in developing reliable computer aided detection and diagnosis endoscopy systems and suggest a pathway for clinical translation of technologies. Whilst endoscopy is a widely used diagnostic and treatment tool for hollow-organs, there are several core challenges often faced by endoscopists, mainly: 1) presence of multi-class artefacts that hinder their visual interpretation, and 2) difficulty in identifying subtle precancerous precursors and cancer abnormalities. Artefacts often affect the robustness of deep learning methods applied to the gastrointestinal tract organs as they can be confused with tissue of interest. EndoCV2020 challenges are designed to address research questions in these remits. In this paper, we present a summary of methods developed by the top 17 teams and provide an objective comparison of state-of-the-art methods and methods designed by the participants for two sub-challenges: i) artefact detection and segmentation (EAD2020), and ii) disease detection and segmentation (EDD2020). Multi-center, multi-organ, multi-class, and multi-modal clinical endoscopy datasets were compiled for both EAD2020 and EDD2020 sub-challenges. The out-of-sample generalization ability of detection algorithms was also evaluated. Whilst most teams focused on accuracy improvements, only a few methods hold credibility for clinical usability. The best performing teams provided solutions to tackle class imbalance, and variabilities in size, origin, modality and occurrences by exploring data augmentation, data fusion, and optimal class thresholding techniques., 32 pages

Verification of properties expressed as-regular languages such as LTL can benefit hugely from stutter-insensitivity, using a diverse set of reduction strategies. However properties that are not stutter-insensitive, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter-insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a reduction of a system. A reduction has the property that it can only shorten runs. Lipton's transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. An implementation and experimental evidence is provided showing most nonrandom properties sensitive to stutter are actually shortening or lengthening insensitive. Performance of experiments on a large (random) benchmark from the model-checking competition indicate that despite being a semi-decision procedure, the approach can still improve state of the art verification tools., Comment: Formal Techniques for Distributed Objects, Components, and Systems FORTE 2022, Jun 2022, Lucia, Italy

Purpose The purpose of this study was to identify in the EPIRMEX cohort the correlations between MRI brain metrics, including diffuse excessive high signal intensities (DEHSI) obtained with an automated quantitative method and neurodevelopmental outcomes at 2 years. Materials and methods A total of 390 very preterm infants (gestational age at birth ≤ 32 weeks) who underwent brain MRI at term equivalent age at 1.5T (n = 338) or 3T (n = 52) were prospectively included. Using a validated algorithm, automated metrics of the main brain surfaces (cortical and deep gray matter, white matter, cerebrospinal fluid) and DEHSI with three thresholds were obtained. Linear adjust regressions were performed to assess the correlation between brain metrics with the ages and stages questionnaire (ASQ) score at 2 years. Results Basal ganglia and thalami, cortex and white matter surfaces positively and significantly correlated with the global ASQ score. For all ASQ sub-domains, basal ganglia and thalami surfaces significantly correlated with the scores. DEHSI was present in 289 premature newborns (74%) without any correlation with the ASQ score. Metrics of DEHSI were greater at 3T than at 1.5T. Conclusion Brain MRI metrics obtained in our multicentric cohort correlate with the neurodevelopmental outcome at 2 years of age. The quantitative detection of DEHSI is not predictive of adverse outcomes. Our automated algorithm might easily provide useful predictive information in daily practice.

International audience; In Mathematical Morphology (MM), dynamics are used to compute markers to proceed for example to watershed-based image decomposition. At the same time, persistence is a concept coming from Persistent Homology (PH) and Morse Theory (MT) and represents the stability of the extrema of a Morse function. Since these concepts are similar on Morse functions, we studied their relationship and we found, and proved, that they are equal on 1D Morse functions. Here, we propose to extend this proof to n-D, n ≥ 2, showing that this equality can be applied to n-D images and not only to 1D functions. This is a step further to show how much MM and MT are related.

International audience; This paper aims at providing an overview of the use of mathematical morphology, in its algebraic setting, in several fields of artificial intelligence (AI). Three domains of AI will be covered. In the first domain, mathematical morphology operators will be expressed in some logics (propositional, modal, description logics) to answer typical questions in knowledge representation and reasoning, such as revision, fusion, explanatory relations, satisfying usual postulates. In the second domain, spatial reasoning will benefit from spatial relations modeled using fuzzy sets and morphological operators, with applications in model-based image understanding. In the third domain, interactions between mathematical morphology and deep learning will be detailed. Morphological neural networks were introduced as an alternative to classical architectures, yielding a new geometry in decision surfaces. Deep networks were also trained to learn morphological operators and pipelines, and morphological algorithms were used as companion tools to machine learning, for pre/post processing or even regularization purposes. These ideas have known a large resurgence in the last few years and new ones are emerging.

This paper presents the final results of the ICDAR 2021 Competition on Historical Map Segmentation (MapSeg), encouraging research on a series of historical atlases of Paris, France, drawn at 1/5000 scale between 1894 and 1937. The competition featured three tasks, awarded separately. Task~1 consists in detecting building blocks and was won by the L3IRIS team using a DenseNet-121 network trained in a weakly supervised fashion. This task is evaluated on 3 large images containing hundreds of shapes to detect. Task~2 consists in segmenting map content from the larger map sheet, and was won by the UWB team using a U-Net-like FCN combined with a binarization method to increase detection edge accuracy. Task~3 consists in locating intersection points of geo-referencing lines, and was also won by the UWB team who used a dedicated pipeline combining binarization, line detection with Hough transform, candidate filtering, and template matching for intersection refinement. Tasks~2 and~3 are evaluated on 95 map sheets with complex content. Dataset, evaluation tools and results are available under permissive licensing at \url{https://icdar21-mapseg.github.io/}., Selected as one of the official competitions for the 16th International Conference on Document Analysis and Recognition (ICDAR 2021), September 5-10, 2021, Lausanne, Switzerland (https://icdar2021.org/). Extra material available at https://icdar21-mapseg.github.io/

International audience; The image and status of beekeeping is being transformed due to the worldwide enthusiasm for honeybees and concern for their future in our changing world. Yet media discussions about honeybees reveal a tension between naturalist and productivist visions of beekeeping, a tension also found in beekeeping development programs. While illustrating how diverse honey production and its socio-technical organization are, our study of Corsica (France) and Souss (Morocco) show that the naturalist/productivist polarization does not transpire in beekeeping itself. Finally, we discuss this tension in the light of ecologization and the importance of the territorial framework in which beekeeping is conducted, which provides a way of moving beyond a generic and polarized vision.

International audience; In discrete topology, we like digitally well-composed (shortly DWC) interpolations because they remove pinches in cubical images. Usual well-composed interpolations are local and sometimes self-dual (they treat in a same way dark and bright components in the image). In our case, we are particularly interested in n-D self-dual DWC interpolations to obtain a purely self-dual tree of shapes. However , it has been proved that we cannot have an n-D interpolation which is at the same time local, self-dual, and well-composed. By removing the locality constraint, we have obtained an n-D interpolation with many properties in practice: it is self-dual, DWC, and in-between (this last property means that it preserves the contours). Since we did not published the proofs of these results before, we propose to provide in a first time the proofs of the two last properties here (DWCness and in-betweeness) and a sketch of the proof of self-duality (the complete proof of self-duality requires more material and will come later). Some theoretical and practical results are given.

International audience; We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an ω-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a latest appearance record principle, and introduces a partial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step.

With the increase of the number of people with moderate to severe visual impairment, monitoring and treatment of vision disorders have become major issues in medicine today. At the Quinze-Vingts national ophthalmology hospital in Paris, two optical benches have been settled in recent years to develop two real-time digital holography techniques for the retina: holographic optical coherence tomography (OCT) and laser Doppler holography. The first reconstructs three-dimensional images, while the second allows visualization of blood flow in vessels. Besides problems inherent to the imaging system itself, optical devices are subject to external disturbance, bringing also difficulties in imaging and loss of accuracy. The main obstacles these technologies face are eye motion and eye aberrations.In this thesis, we have introduced several methods for image quality improvement in digital holography, and validated them experimentally. The resolution of holographic images has been improved by robust non-iterative methods: lateral and axial tracking and compensation of translation movements, and measurement and compensation of optical aberrations. This allows us to be optimistic that structures on holographic images of the retina will be more visible and sharper, which could ultimately provide very valuable information to clinicians.; Avec l’augmentation du nombre de personnes souffrant de déficience visuelle modérée à sévère, la surveillance et le traitement des troubles de la vision sont devenus des enjeux majeurs de la médecine actuelle. Au centre hospitalier national d’ophtalmologie des Quinze-Vingts à Paris, deux bancs optiques ont été installés ces dernières années pour développer deux techniques d'holographie numérique en temps-réel pour l’imagerie de la rétine : la tomographie holographique par cohérence optique (OCT holographique) plein champ et l'holographie laser Doppler. La première reconstitue des images en trois dimensions, tandis que la seconde permet de visualiser le flux sanguin dans les vaisseaux. Outre les problèmes inhérents au système d'imagerie lui-même, les appareils optiques sont soumis à des perturbations externes, ce qui entraîne également des difficultés d'imagerie et une perte de résolution. Les principaux obstacles auxquels ces technologies sont confrontées sont le mouvement des yeux et les aberrations oculaires. Dans cette thèse, nous avons étudié plusieurs méthodes d'amélioration de la qualité des images en holographie numérique, et les avons validées expérimentalement. La résolution des images holographiques a été améliorée par des méthodes non itératives robustes : compensation des mouvements et mesure et compensation des aberrations optiques. Ce travail ouvre la voie à de nouvelles méthodes de traitement qui permettront une amélioration majeure de la résolution des images en holographie numérique de la rétine, et qui pourront fournir des informations très précieuses aux cliniciens, à terme.

In this paper, we prove that the two avours of well-compo- sedness called Continuous Well-Composedness (shortly CWCness), stat- ing that the boundary of the continuous analog of a discrete set is a manifold, and Digital Well-Composedness (shortly DWCness), stating that a discrete set does not contain any critical con guration, are not equivalent in dimension 4. To prove this, we exhibit the example of a con- guration of 8 tesseracts (4D cubes) sharing a common corner (vertex), which is DWC but not CWC. This result is surprising since we know that CWCness and DWCness are equivalent in 2D and 3D. To reach our goal, we use local homology.

This habilitation report relates the computer science research done since 2006 at the EPITA Research and Development Laboratory (LRDE). This research deals with dynamic programming languages, and more specifically their expressivity and performance.

Because the NIS reports hospital discharges rather than unique patients, we were unable to identify patients with multiple hospitalizations or estimate the per-person costs of hepatitis A inpatient care. We were also not able to separately report the costs associated with liver transplantation. Even though using highly sensitive inclusion criteria might have introduced an element of cost over-estimation in some patients incidentally diagnosed with hepatitis A while admitted for other conditions, our results almost certainly underestimate hospitalization costs associated with the ongoing hepatitis A outbreaks because NIS does not include hospital-based physician fees. Moreover, the national $306.8 million estimate does not account for outpatient visits , emergency department visits that did not result in an admission to the same hospital, lost productivity , out-of-pocket costs to patients or their informal caregivers, or public health costs associated with the hepatitis A outbreaks, further reinforcing the conservative nature of this estimate. Given the high proportion of hospitalized patients during the ongoing hepatitis A outbreaks, we estimated the average hepatitis A-related hospitalization costs to highlight the preventable economic burden of these outbreaks on healthcare systems and state governments. Hepatitis A is a vaccine-preventable disease. Despite longstanding vaccination recommendations for adults at increased risk for hepatitis A virus infection or adverse consequences of infection, self-reported adult hepatitis A vaccination coverage with >2 doses was only 10.9% for persons >19 years of age in 2017 (6). Our findings underscore the importance of improving hepatitis A vaccination coverage among at-risk adults, in accordance with Advisory Committee on Immunization Practices recommendations (7).

International audience; Making the most of multispectral image time-series is a promising but still relatively under-explored research direction because of the complexity of jointly analyzing spatial, spectral and temporal information. Capturing and characterizing temporal dynamics is one of the important and challenging issues. Our new method paves the way to capture real data dynamics and should eventually benefit applications like unmixing or classification. Dealing with time-series dynamics classically requires the knowledge of a dynamical model and an observation model. The former may be incorrect or computationally hard to handle, thus motivating data-driven strategies aiming at learning dynamics directly from data. In this paper, we adapt neural network architectures to learn periodic dynamics of both simulated and real multispectral time-series. We emphasize the necessity of choosing the right state variable to capture periodic dynamics and show that our models can reproduce the average seasonal dynamics of vegetation using only one year of training data.

International audience; We present in this paper a new approach to the static analysis of concurrent programs with procedures. To this end, we model multi-threaded programs featuring recursive procedure calls and synchronisation by rendezvous between parallel threads with communicating pushdown systems (from now on CPDSs). The reachability problem for this particular class of automata is unfortunately undecidable. However, it has been shown that an efficient abstraction of the execution traces language can nonetheless be computed. To this end, an algebraic framework to over-approximate context-free languages has been introduced by Bouajjani et al. In this paper, we combine this framework with an automata-theoretic approach in order to approximate an answer to the model checking problem of the lineartime temporal logic (from now on LTL) on CPDSs. We then present an algorithm that, given a single-indexed or stutter-invariant LTL formula, allows us to prove that no run of a CPDS verifies this formula if the procedure ends.

International audience; In explicit state model checking of concurrent systems, multi-core emptiness checks and partial order reductions (POR) are two major techniques to handle large state spaces. The first one tries to take advantage of multi-core architectures while the second one may decrease exponentially the size of the state space to explore. For checking LTL properties, Bloemen and van de Pol [2] shown that the best performance is currently obtained using their multi-core SCC-based emptiness check. However, combining the latest SCC-based algorithm with POR is not trivial since a condition on cycles, the proviso, must be enforced on an algorithm which processes collaboratively cycles. In this paper, we suggest a pessimistic approach to tackle this problem for liveness properties. For safety ones, we propose an algorithm which takes benefit from the information computed by the SCC-based algorithm. We also present new parallel provisos for both safety and liveness properties that relies on other multi-core emptiness checks. We observe that all presented algorithms maintain good reductions and scalability.

International audience; The measurement of medical images can be hindered by blur and distortions caused by the physiological motion. Specially for retinal imaging, images are greatly affected by sharp movements of the eye. Stabilization methods have been developed and applied to state-of-the-art retinal imaging modalities ; here we intend to adapt them for coherent light detection schemes. In this paper, we demonstrate experimentally cross-correlation-based lateral and axial motion compensation in laser Doppler imaging and optical coherence tomography by digital holography. Our methods improve lateral and axial image resolution in those innovative instruments and allow a better visualization during motion.

International audience; Over the last decade, parallel SATisfiability solving has been widely studied from both theoretical and practical aspects. There are two main approaches. First, divide-and-conquer (D&C) splits the search space, each solver being in charge of a particular subspace. The second one, portfolio launches multiple solvers in parallel, and the first to find a solution ends the computation. However although D&C based approaches seem to be the natural way to work in parallel, portfolio ones experimentally provide better performances. An explanation resides on the difficulties to use the native formulation of the SAT problem (i.e., the CNF form) to compute an apriori good search space partitioning (i.e.,all parallel solvers process their sub-spaces in comparable computational time). To avoid this, dynamic load balancing of the search subspaces is implemented. Unfortunately, this isdifficult to compare load balancing strategies since state-of-the-art SAT solvers appropriately dealing with these aspects are hardly adaptable tovarious strategies than the ones they have been designed for. This paper aims at providing a way to overcome this problem by proposing an implementation and evaluation of different types of divide-and-conquer inspired from the literature. These are relying on thePainless framework, which provides concurrent facilities to elaborate such parallel SAT solvers. Comparison of the various strategies are thendiscussed.

International audience; Quickref is a global documentation project for Common Lisp software. It builds a website containing reference manuals for Quicklisp libraries. Each library is first compiled, loaded, and introspected. From the collected information, a Texinfo le is generated, which is then processed into HTML. Because of the large number of libraries in Quicklisp, doing this sequentially may require several hours of processing. We report on our experiments parallelizing Quickref. Experimental data on the morphology of Quicklisp libraries has been collected. Based on this data, we are able to propose a number of parallelization schemes that reduce the total processing time by a factor of 3.8 to 4.5, depending on the exact situation.

In this paper, we propose a fast automatic method that segments left atrial cavity from 3D GE-MRIs without any manual assistance, using a fully convolutional network (FCN) and transfer learning. This FCN is the base network of VGG-16, pre-trained on ImageNet for natural image classification, and fine tuned with the training dataset of the MICCAI 2018 Atrial Segmentation Challenge. It relies on the “pseudo-3D” method published at ICIP 2017, which allows for segmenting objects from 2D color images which contain 3D information of MRI volumes. For each \(n^{\text {th}}\) slice of the volume to segment, we consider three images, corresponding to the \((n-1)^{\text {th}}\), \(n^{\text {th}}\), and \((n+1)^{\text {th}}\) slices of the original volume. These three gray-level 2D images are assembled to form a 2D RGB color image (one image per channel). This image is the input of the FCN to obtain a 2D segmentation of the \(n^{\text {th}}\) slice. We process all slices, then stack the results to form the 3D output segmentation. With such a technique, the segmentation of the left atrial cavity on a 3D volume takes only a few seconds. We obtain a Dice score of 0.92 both on the training set in our experiments before the challenge, and on the test set of the challenge.

International audience; In computational imaging by digital holography, lateral resolution of retinal images is limited to about 20 microns by the aberrations of the eye. To overcome this limitation, the aberrations have to be canceled. Digital aberration compensation can be performed by post-processing of full-field digital holograms. Aberration compensation was demonstrated from wavefront measurement by reconstruction of digital holograms in subapertures [1], and by measurement of a guide star hologram [2]. Yet, these wavefront measurement methods have limited accuracy in practice. For holographic tomography of the human retina, image reconstruction was demonstrated by iterative digital aberration compensation, by minimization of the local entropy of speckle-averaged tomographic volumes [3]. However image-based aberration compensation is time-consuming, preventing real-time image rendering. We are investigating a new digital aberration compensation scheme with a deep neural network to circumvent the limitations of these aberrations correction methods. To train the network, 28.000 anonymized images of eye fundus from patients of the 15-20 hospital in Paris have been collected, and synthetic interferograms have been reconstructed digitally by simulating the propagation of eye fundus images recorded with standard cameras. With a U-Net architecture [4], we demonstrate defocus correction of these complex-valued synthetic interferograms. Other aberration orders will be corrected with the same method, to improve lateral resolution up to the diffraction limit in digital holo-graphic imaging of the retina.The measurement of medical images can be hindered by blur and distortions caused by the physiological motion. Specially for retinal imaging, images are greatly affected by sharp movements of the eye. Stabilization methods have been developed and applied to state-of-the-art retinal imaging modalities; here we intend to adapt them for coherent light detection schemes. In this paper , we demonstrate experimentally cross-correlation-based lateral and axial motion compensation in laser Doppler imaging and optical coherence tomography by digital holography. Our methods improve lateral and axial image resolution in those innovative instruments and allow a better visualization during motion.

We state in this paper a strong relation existing between Mathematical Morphology and Discrete Morse Theory when we work with 1D Morse functions. Specifically, in Mathematical Morphology, a classic way to extract robust markers for segmentation purposes, is to use the dynamics. On the other hand, in Discrete Morse Theory, a well-known tool to simplify the Morse-Smale complexes representing the topo-logical information of a Morse function is the persistence. We show that pairing by persistence is equivalent to pairing by dynamics. Furthermore, self-duality and injectivity of these pairings are proved.

Fast advancement of machine learning methods and constant growth of the areas of application open up new horizons for large data management and processing. Among the various types of data available for analysis, the Fourier Transform InfraRed (FTIR) spectroscopy spectra are very challenging datasets to consider. In this study, machine learning is used to analyze and predict a rheological parameter: firmness. Various statistics have been gathered including both chemistry (such as ethylene, titrable acidity or sugars) and spectra values to visualize and analyze a dataset of 731 biological samples. Two-dimensional (2D) and three-dimensional (3D) principal component analyses (PCA) are used to evaluate their ability to discriminate for one parameter: firmness. Partial least squared regression (PLSR) modeling has been carried out to predict the rheological parameter using either sixteen physicochemical parameters or only the infrared spectra. We show that (i) the spectra alone allows good discrimination of the samples based on rheology, (ii) 3D-PCA allows comprehensive and informative visualization of the data, and (iii) that the rheological parameters are predicted accurately using a regression method such as PLSR; instead of using chemical parameters which are laborious to obtain, Mid-FTIR spectra gathering all physicochemical information could be used for efficient prediction of firmness. As a conclusion, rheological and chemical parameters allow good discrimination of the samples according to their firmness. However, using only the IR spectra leads to better results. A good predictive model was built for the prediction of the firmness of the fruit, and we reached a coefficient of determination R2 value of 0.90. This method outperforms a model based on physicochemical descriptors only. Such an approach could be very helpful to technologists and farmers.

International audience; Spherical fluorescent particle are micrometer-scale spherical beads used in various areas of physics, chemistry or biology as markers associated with local physical media. They are useful for example in fluid dynamics to characterize flows, diffusion coefficients, viscosity or temperature ; they are used in cells dynamics to estimate mechanical strain and stress at the micrometer scale. In order to estimate these physical measurements , tracking these particles is necessary. Numerous approaches and existing packages, both open-source and proprietary are available to achieve tracking with a high degree of precision in 2D. However, little such software is available to achieve tracking in 3D. One major difficulty is that 3D confocal microscopy acquisition is not typically fast enough to assume that the beads are stationary during the whole 3D scan. As a result, beads may move between planar scans. Classical approaches to 3D segmentation may yield objects are not spherical. In this article, we propose a 3D bead segmentation that deals with this situation.

International audience; In 2013, Najman and Géraud proved that by working on a well-composed discrete representation of a gray-level image, we can compute what is called its tree of shapes, a hierarchical representation of the shapes in this image. This way, we can proceed to morphological filtering and to image segmentation. However , the authors did not provide such a representation for the non-cubical case. We propose in this paper a way to compute a well-composed representation of any gray-level image defined on a discrete surface, which is a more general framework than the usual cubical grid. Furthermore, the proposed representation is self-dual in the sense that it treats bright and dark components in the image the same way. This paper can be seen as an extension to gray-level images of the works of Daragon et al. on discrete surfaces.

The inclusion and adjacency relationship between image regions usually carry contextual information. The later is widely used since it tells how regions are arranged in images. The former is usually not taken into account although it parallels the object-background relationship. The mathematical morphology framework provides several hierarchical image representations. They include the Tree of Shapes (ToS), which encodes the inclusion of level-line, and the hierarchies of segmentation (e.g., alpha-tree, BPT), which is useful in the analysis of the adjacency relationship. In this work, we take advantage of both inclusion and adjacency information in these representations for computer vision applications. We introduce the spatial alignment graph w.r.t inclusion that is constructed by adding a new adjacency relationship to nodes of the ToS. In a simple ToS such as our Tree of Shapes of Laplacian sign, which encodes the inclusion of Morphological Laplacian 0-crossings, the graph is reduced to a disconnected graph where each connected component is a semantic group. In other cases, e.g., classic ToS, the spatial alignment graph is more complex. To address this issue, we expand the shape-spaces morphology. Our expansion has two primary results: 1)It allows the manipulation of any graph of shapes. 2)It allows any tree filtering strategy proposed by the connected operators frameworks. With this expansion, the spatial graph could be analyzed with the help of an alpha-tree. We demonstrated the application aspect of our method in the application of text detection. The experiment results show the efficiency and effectiveness of our methods, which is appealing to mobile applications., Les relations d'inclusion et d'adjacence des regions dans l'images comportent des informations contextuelles. Le relation d'adjacence est largement utilisé car il indique comment les régions sont organisées dans l'images. La relation d'inclusion n'est généralement pas prise en compte, bien qu'il assimile la relation d'objet-fond. Il existe plusieurs représentations morphologiques hiérarchiques: l'arbre des formes (AdF) qui représentent l'inclusion de lignes de niveaux d'image, ainsi que les hiérarchies de segmentation (i.e. la hiérarchie des quasi-zones plates) qui est utile dans l'analyse de la relation d'adjacence. Le but de ce travail est de tirer partie à la fois des relations d’inclusion et d’adjacence dans ces representations pour mener à bien des tâches de vision par ordinateur. Nous introduisons le graphe d'alignement spatial (GAS) qui est construit à partir de l'inclusion et de l'arrangement spatial des régions dans l'AdF. Dans un cas simple tel que notre l'AdF de Laplacien, le GAS est réduit à un graphe déconnecté où chaque composant connecté est un groupe sémantique d'objets. Dans d’autres cases, e.g., l'AdF classique, le GAS est plus complexe. Pour résoudre ce problème, nous proposons d'élargir notre raisonnement à la morphologie basée sur la forme. Notre extension permet de manipuler n'importe quel graphe des formes et permet n'importe stratégie de filtrage dans la cadre de opérateurs connexes. Par conséquent, le GAS pourrait être analysé par une hiérarchie des quasi-zones plates. Les résultats de notre méthode dans la reconnaissance de texte montrent l'efficacité et la performance, qui sont attrayantes notablement pour les applications mobiles.

The inclusion and adjacency relationship between image regions usually carry contextual information. The later is widely used since it tells how regions are arranged in images. The former is usually not taken into account although it parallels the object-background relationship. The mathematical morphology framework provides several hierarchical image representations. They include the Tree of Shapes (ToS), which encodes the inclusion of level-line, and the hierarchies of segmentation (e.g., alpha-tree, BPT), which is useful in the analysis of the adjacency relationship. In this work, we take advantage of both inclusion and adjacency information in these representations for computer vision applications. We introduce the spatial alignment graph w.r.t inclusion that is constructed by adding a new adjacency relationship to nodes of the ToS. In a simple ToS such as our Tree of Shapes of Laplacian sign, which encodes the inclusion of Morphological Laplacian 0-crossings, the graph is reduced to a disconnected graph where each connected component is a semantic group. In other cases, e.g., classic ToS, the spatial alignment graph is more complex. To address this issue, we expand the shape-spaces morphology. Our expansion has two primary results: 1)It allows the manipulation of any graph of shapes. 2)It allows any tree filtering strategy proposed by the connected operators frameworks. With this expansion, the spatial graph could be analyzed with the help of an alpha-tree. We demonstrated the application aspect of our method in the application of text detection. The experiment results show the efficiency and effectiveness of our methods, which is appealing to mobile applications.; Les relations d'inclusion et d'adjacence des regions dans l'images comportent des informations contextuelles. Le relation d'adjacence est largement utilisé car il indique comment les régions sont organisées dans l'images. La relation d'inclusion n'est généralement pas prise en compte, bien qu'il assimile la relation d'objet-fond. Il existe plusieurs représentations morphologiques hiérarchiques: l'arbre des formes (AdF) qui représentent l'inclusion de lignes de niveaux d'image, ainsi que les hiérarchies de segmentation (i.e. la hiérarchie des quasi-zones plates) qui est utile dans l'analyse de la relation d'adjacence. Le but de ce travail est de tirer partie à la fois des relations d’inclusion et d’adjacence dans ces representations pour mener à bien des tâches de vision par ordinateur. Nous introduisons le graphe d'alignement spatial (GAS) qui est construit à partir de l'inclusion et de l'arrangement spatial des régions dans l'AdF. Dans un cas simple tel que notre l'AdF de Laplacien, le GAS est réduit à un graphe déconnecté où chaque composant connecté est un groupe sémantique d'objets. Dans d’autres cases, e.g., l'AdF classique, le GAS est plus complexe. Pour résoudre ce problème, nous proposons d'élargir notre raisonnement à la morphologie basée sur la forme. Notre extension permet de manipuler n'importe quel graphe des formes et permet n'importe stratégie de filtrage dans la cadre de opérateurs connexes. Par conséquent, le GAS pourrait être analysé par une hiérarchie des quasi-zones plates. Les résultats de notre méthode dans la reconnaissance de texte montrent l'efficacité et la performance, qui sont attrayantes notablement pour les applications mobiles.

Ancient maps are an historical and cultural heritage widely recognized as a very important source of information, but exploiting such maps is complicated. In this project, we consider the Linguistic Atlas of France (ALF), built between 1902 and 1910. This cartographical heritage produces firstrate data for dialectological researches. In this paper, we focus on the separation of the content in layers for facilitating the extraction, the analysis, the visualization and the diffusion of the data contained in these ancient linguistic atlases.

This thesis presents code generation techniques related to run-time type checking of heterogeneous but regular sequences. We generalize traditional regular expressions to accommodate surface syntax, internal representation, computation, optimization, and serialization (code generation) of rational type expressions. We explore traditional s-expression based representation contrasted with Binary Decision Diagrams which have been enhanced to represent Boolean operations in a type lattice supporting subtyping. We introduce the Maximal Disjoint Type Decomposition, prove the existence and uniqueness of a solution, and further explore several alternative algorithms for calculating it. The Maximal Disjoint Type Decomposition is used to generate a deterministic finite automaton representing a rational type expression, after which compile-time code is generated which will perform run-time type membership checks. Such code generation risks dealing with redundant type checks. We further investigate these potential problems and again use the theory of Binary Decision Diagrams to eliminate these redundant checks to produce optimized type checking code. The techniques and algorithms introduced and discussed in this thesis explore representations and computations dealing with type based computations in dynamic programming languages.; Cette thèse présente des techniques de génération de code liées à la vérification dynamique de types de séquences hétérogènes mais régulières. Nous généralisons les expressions rationnelles classiques aux expressions rationnelles de type, en adaptant leur surface syntaxique, représentation interne, calcul, optimisation, et sérialisation (génération de code). Nous comparons la forme native basée sur des S-Expressions avec une représentation par Diagrammes de Décision Binaire, enrichis pour représenter les opérations booléennes dans un treillis de types prenant en charge le sous-typage. Nous introduisons alors la notion de Décomposition Maximale en Types Disjoints, nous prouvons l'existence et l'unicité d'une telle décomposition, et nous explorons plusieurs solutions algorithmiques pour calculer celle-ci. La Décomposition Maximale en Types Disjoints est utilisée pour générer un automate fini et déterministe représentant une expression rationnelle de type. Cet automate est utilisé à la compilation pour générer à son tour du code de vérification dynamique de type. Le code ainsi généré ne tient a priori pas compte d'éventuelles redondances dans les vérifications de type. Nous étudions donc ces problèmes plus en détail et utilisons à nouveau la théorie des Diagrammes de Décision Binaire afin d'éliminer les calculs redondants et de produire ainsi du code optimisé. Le travail présenté dans cette thèse s'attache à traiter des problèmes de représentations et de calcul sur des types dans les langages dynamiques.

International audience; We summarize a technique for writing functions which recognize types of heterogeneous sequences in Common Lisp. The technique employs sequence recognition functions, generated at compile time, and evaluated at run-time. The technique we demonstrate extends the Common Lisp type system, exploiting the theory of rational languages, Binary Decision Diagrams, and the Turing complete macro facility of Common Lisp. The resulting system uses meta-programming to move an Ω(2 n) complexity operation from run-time to a compile-time operation, leaving a highly optimized Θ(n) complexity operation for run-time.

Publisher's version (útgefin grein), Component trees are region-based representations that encode the inclusion relationship of the threshold sets of an image. These representations are one of the most promising strategies for the analysis and the interpretation of spatial information of complex scenes as they allow the simple and efficient implementation of connected filters. This work proposes a new efficient hybrid algorithm for the parallel computation of two particular component trees—the max- and min-tree—in shared and distributed memory environments. For the node-local computation a modified version of the flooding-based algorithm of Salembier is employed. A novel tuple-based merging scheme allows to merge the acquired partial images into a globally correct view. Using the proposed approach a speed-up of up to 44.88 using 128 processing cores on eight-bit gray-scale images could be achieved. This is more than a five-fold increase over the state-of-the-art shared-memory algorithm, while also requiring only one-thirty-second of the memory., The authors would like to thank Igancio Toledo and Martin Kornmesser for making the ESO/VVV Survey/D. Minniti image with the id eso1242a publicly available.

International audience; This paper presents a pedestrian navigation algorithm based on a foot-mounted 9-DOF Inertial Measurement Unit (IMU), which provides tri-axial accelerations, angular rates and magnetics. Most of algorithms used worldwide employ Zero Velocity Update (ZUPT) to reduce the tremendous error of integration from acceleration to displacement. The crucial part in ZUPT is to detect stance phase precisely, a cyclic left-to-right style Hidden Markov Model is introduced in this work which is able to appropriately model the periodic nature of signals. Stance detection is then made unsupervised by using a suited learning algorithm. Then orientation estimation is performed independently by a quaternion-based method, a simplified error-state Extended Kalman Filter (EKF) assists trajectory reconstruction in 3D space, neither extra method nor prior knowledge is needed to estimate the height. Experimental results on large free-walking trajectories show that the proposed algorithm can provide more accurate locations, especially in z-axis compared to competitive algorithms, w.r.t. to a ground-truth obtained using OpenStreetMap.

International audience; Modern computing systems have grown in complexity, and the attack surface has increased accordingly. Even though system components are generally carefully designed and even verified by different groups of people, the composition of these components is often regarded with less attention. This paves the way for " architectural attacks " , a class of security vulnerabilities where the attacker is able to threaten the security of the system even if each of its components continues to act as expected. In this article, we introduce FreeSpec, a formalism built upon the key idea that components can be modelled as programs with algebraic effects to be realized by other components. FreeSpec allows for the modular modelling of a complex system, by defining idealized components connected together, and the modular verification of the properties of their composition. In addition, we have implemented a framework for the Coq proof assistant based on FreeSpec.

International audience; Some modern processors include decimal floating-point units, with a conforming implementation of the IEEE-754 2008 standard. Unfortunately, many algorithms from the computer arithmetic literature are not correct anymore when computations are done in radix 10. This is in particular the case for the computation of the average of two floating-point numbers. Several radix-2 algorithms are available, including one that provides the correct rounding, but none hold in radix 10. This paper presents a new radix-10 algorithm that computes the correctly-rounded average. To guarantee a higher level of confidence, we also provide a Coq formal proof of our theorems, that takes gradual underflow into account. Note that our formal proof was generalized to ensure this algorithm is correct when computations are done with any even radix.

National audience

International audience; This paper presents a pedestrian navigation algorithm based on a foot-mounted 9DOF Inertial Measurement Unit, which provides accelerations, angular rates and magnet-ics along 3-axis during the motion. Most of algorithms used worldwide are based on stance detection to reduce the tremendous integration errors, from acceleration to displacement. As the crucial part is to detect stance phase precisely, we introduced a cyclic left-to-right style Hidden Markov Model that is able to appropriately model the periodic nature of signals. Stance detection is then made unsupervised by using a suited learning algorithm. Then, assisted by a simplified error-state Kalman filter, trajectory can be reconstructed. Experimental results show that the proposed algorithm can provide more accurate location, compared to competitive algorithms, w.r.t. ground-truth obtained from OpenStreet Map.

International audience; SAT solvers are now widely used to solve a large variety of problems, including formal verification of systems. SAT problems derived from such applications often exhibit symmetry properties that could be exploited to speed up their solving. Static symmetry breaking is so far the most popular approach to take advantage of symmetries. It relies on a symmetry preprocessor which augments the initial problem with constraints that force the solver to consider only a few configurations among the many symmetric ones. This paper presents a new way to handle symmetries, that avoid the main problem of the current static approaches: the prohibitive cost of the preprocessing phase. Our proposal has been implemented in MiniSym. Extensive experiments on the benchmarks of last six SAT competitions show that our approach is competitive with the best state-of-the-art static symmetry breaking solutions.