La connaissance du niveau de bruit dans une image est précieuse pour de nombreuses applications en traitement d’images. L’estimation de la fonction de niveau de bruit requiert l’identification des zones homogènes sur lesquelles les paramètres du bruit peuvent être calculés. Sutour et al. en 2015 ont proposé une méthode d’estimation de la fonction de niveau de bruit se basant sur la recherche de zones homogènes de forme carrée, donc inadaptées au contenu local de l’image. Nous généralisons cette méthode à la recherche de zones homogènes de forme quelconque en nous basant sur la représentation par arbre des formes de l’image étudiée, permettant ainsi une estimation plus robuste de la fonction de niveau de bruit.

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 topological 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.

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 component trees provide a high-level, hierarchical, and contrast invariant representations of images, suitable for many image processing tasks. Yet their definition is ill-formed on multivariate data, e.g., color images, multi-modality images, multi-band images, and so on. Common workarounds such as marginal processing, or imposing a total order on data are not satisfactory and yield many problems, such as artifacts, loss of invariances, etc. In this paper, inspired by the way the Multivariate Tree of Shapes (MToS) has been defined, we propose a definition for a Multivariate min-tree or max-tree. We do not impose an arbitrary total ordering on values; we use only the inclusion relationship between components. As a straightforward consequence, we thus have a new class of multivariate connected openings and closings.

Boolean SATisfiability has been used successfully in many applicative contexts. This is due to the capability of modern SAT solvers to solve complex problems involving millions of variables. Most SAT solvers have long been sequential and based on the CDCL algorithm. The emergence of many-core machines opens new possibilities in this domain. There are numerous parallel SAT solvers that differ by their strategies, programming languages, etc. Hence, comparing the efficiency of the theoretical approaches in a fair way is a challenging task. Moreover, the introduction of a new approach needs a deep understanding of the existing solvers’ implementations. We present Painless: a framework to build parallel SAT solvers for many-core environments. Thanks to its genericness and modularity, it provides the implementation of basics for parallel SAT solving. It also enables users to easily create their parallel solvers based on new strategies. Painless allowed to build and test existing strategies by using different chunk of solutions present in the literature. We were able to easily mimic the behaviour of three state-of-the-art solvers by factorising many parts of their implementations. The efficiency of Painless was highlighted as these implementations are at least efficient as the original ones. Moreover, one of our solvers won the SAT Competition’18. Going further, Painless enabled to conduct fair experiments in the context of divide-and-conquer solvers, and allowed us to highlight original compositions of strategies performing better than already known ones. Also, we were able to create and test new original strategies exploiting the modular structure of SAT instances.

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.

Braids of partitions have been introduced in a theoretical framework as a generalization of hierarchies of partitions, but practical guidelines to derive such structures remained an open question. In a previous work, we proposed a methodology to build a braid of partitions by experimentally composing cuts extracted from two hierarchies of partitions, notably paving the way for the hierarchical representation of multimodal images. However, we did not provide the formal proof that our proposed methodology was yielding a braid structure. We remedy to this point in the present paper and give a brief insight on the structural properties of the resulting braid of partitions.

In the automata theoretic approach to explicit state LTL model checking, the synchronized product of the model and an automaton that represents the negated formula is checked for emptiness. In practice, a (transition-based generalized) Büchi automaton (TGBA) is used for this procedure.This paper investigates whether using a more general form of acceptance, namely a transition-based generalized Rabin automaton (TGRA), improves the model checking procedure. TGRAs can have significantly fewer states than TGBAs, however the corresponding emptiness checking procedure is more involved. With recent advances in probabilistic model checking and LTL to TGRA translators, it is only natural to ask whether checking a TGRA directly is more advantageous in practice.We designed a multi-core TGRA checking algorithm and performed experiments on a subset of the models and formulas from the 2015 Model Checking Contest and generated LTL formulas for models from the BEEM database. While we found little to no improvement by checking TGRAs directly, we show how various aspects of a TGRA’s structure influences the model checking performance.In this paper, we also introduce a Fin-less acceptance condition, which is a disjunction of TGBAs. We show how to convert TGRAs into automata with Fin-less acceptance and show how a TGBA emptiness procedure can be extended to check Fin-less automata.

As there are as many clients as many usages of an Image Processing library, each one may expect different services from it. Some clients may look for efficient and production-quality algorithms, some may look for a large tool set, while others may look for extensibility and genericity to inter-operate with their own code base... but in most cases, they want a simple-to-use and stable product. For a C++ Image Processing library designer, it is difficult to conciliate genericity, efficiency and simplicity at the same time. Modern C++ (post 2011) brings new features for library developers that will help designing a software solution combining those three points. In this paper, we develop a method using these facilities to abstract the library components and augment the genericity of the algorithms. Furthermore, this method is not specific to image processing; it can be applied to any C++ scientific library.

The work presented in this paper addresses the MICCAI BraTS 2019 challenge devoted to brain tumor segmentation using mag- netic resonance images. For each task of the challenge, we proposed and submitted for evaluation an original method. For the tumor segmentation task (Task 1), our convolutional neural network is based on a variant of the U-Net architecture of Ronneberger et al. with two modifications: first, we separate the four convolution parts to decorrelate the weights corresponding to each modality, and second, we provide volumes of size 240 * 240 * 3 as inputs in these convolution parts. This way, we profit of the 3D aspect of the input signal, and we do not use the same weights for separate inputs. For the overall survival task (Task 2), we compute explainable features and use a kernel PCA embedding followed by a Random Forest classifier to build a predictor with very few training samples. For the uncertainty estimation task (Task 3), we introduce and compare lightweight methods based on simple principles which can be applied to any segmentation approach. The overall performance of each of our contribution is honorable given the low computational requirements they have both for training and testing.