Publications

A new minimum barrier distance for multivariate images with applications to salient object detection, shortest path finding, and segmentation

Abstract

Distance transforms and the saliency maps they induce are widely used in image processing, computer vision, and pattern recognition. One of the most commonly used distance transform is the geodesic one. Unfortunately, this distance does not always achieve satisfying results on noisy or blurred images. Recently, a new (pseudo-)distance, called the minimum barrier distance (MBD), more robust to pixel variations, has been introduced. Some years after, Géraud et al. have proposed a good and fast-to compute approximation of this distance: the Dahu pseudo-distance. Since this distance was initially developped for grayscale images, we propose here an extension of this transform to multivariate images; we call it vectorial Dahu pseudo-distance. An efficient way to compute it is provided in this paper. Besides, we provide benchmarks demonstrating how much the vectorial Dahu pseudo-distance is more robust and competitive compared to other MB-based distances, which shows how much this distance is promising for salient object detection, shortest path finding, and object segmentation.

Continue reading

Improving swarming using genetic algorithms

Abstract

The verification of temporal properties against a given system may require the exploration of its full state space. In explicit model checking, this exploration uses a depth-first search and can be achieved with multiple randomized threads to increase performance. Nonetheless, the topology of the state space and the exploration order can cap the speedup up to a certain number of threads. This paper proposes a new technique that aims to tackle this limitation by generating artificial initial states, using genetic algorithms. Threads are then launched from these states and thus explore different parts of the state space. Our prototype implementation is 10% faster than state-of-the-art algorithms on a general benchmark and 40% on a specialized benchmark. Even if we expected a decrease in an order of magnitude, these results are still encouraging since they suggest a new way to handle existing limitations. Empirically, our technique seems well suited for “linear topology”, i.e., the one we can obtain when combining model checking algorithms with partial-order reduction techniques.

Continue reading

Community and LBD-based clause sharing policy for parallel SAT solving

Abstract

Modern parallel SAT solvers rely heavily on effective clause sharing policies for their performance. The core problem being addressed by these policies can be succinctly stated as “the problem of identifying high-quality learnt clauses” that when shared between the worker nodes of parallel solvers results in improved performance than otherwise. The term “high-quality clauses” is often defined in terms of metrics that solver designers have identified over years of empirical study. Some of the more well-known metrics to identify high-quality clauses for sharing include clause length, literal block distance (LBD), and clause usage in propagation. In this paper, we propose a new metric aimed at identifying high-quality learnt clauses and a concomitant clause-sharing policy based on a combination of LBD and community structure of Boolean formulas. The concept of community structure has been proposed as a possible explanation for the extraordinary performance of SAT solvers in industrial instances. Hence, it is a natural candidate as a basis for a metric to identify high-quality clauses. To be more precise, our metric identifies clauses that have low LBD and low community number as ones that are high-quality for applications such as verification and testing. The community number of a clause C measures the number of different communities of a formula that the variables in C span. We perform extensive empirical analysis of our metric and clause-sharing policy, and show that our method significantly outperforms state-of-the-art techniques on the benchmark from the parallel track of the last four SAT competitions.

Continue reading

Using separated inputs for multimodal brain tumor segmentation with 3D U-Net-like architectures

Abstract

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.

Continue reading

LTL model checking for communicating concurrent programs

Abstract

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 rendez-vous 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 linear-time 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.

Continue reading

Seminator 2 can complement generalized Büchi automata via improved semi-determinization

Abstract

We present the second generation of the tool Seminator that transforms transition-based generalized Büchi automata (TGBAs) into equivalent semi-deterministic automata. The tool has been extended with numerous optimizations and produces considerably smaller automata than its first version. In connection with the state-of-the-art LTL to TGBAs translator Spot, Seminator 2 produces smaller (on average) semi-deterministic automata than the direct LTL to semi-deterministic automata translator ltl2ldgba of the Owl library. Further, Seminator 2 has been extended with an improved NCSB complementation procedure for semi-deterministic automata, providing a new way to complement automata that is competitive with state-of-the-art complementation tools.

Continue reading

Experimental digital gabor hologram rendering of C. Elegans worms by a model-trained convolutional neural network (conference presentation)

Abstract

Continue reading

A new minimum barrier distance for multivariate images with applications to salient object detection, shortest path finding, and segmentation

Abstract

Hierarchical image representations are widely used in image processing to model the content of an image in the multi-scale structure. A well-known hierarchical representation is the tree of shapes (ToS) which encodes the inclusion relationship between connected components from different thresholded levels. This kind of tree is self-dual, contrast-change invariant and popular in computer vision community. Typically, in our work, we use this representation to compute the new distance which belongs to the mathematical morphology domain. Distance transforms and the saliency maps they induce are generally used in image processing, computer vision, and pattern recognition. One of the most commonly used distance transforms is the geodesic one. Unfortunately, this distance does not always achieve satisfying results on noisy or blurred images. Recently, a new pseudo-distance, called the minimum barrier distance (MBD), more robust to pixel fluctuation, has been introduced. Some years after, Géraud et al. have proposed a good and fast-to-compute approximation of this distance: the Dahu pseudo-distance. Since this distance was initially developed for grayscale images, we propose here an extension of this transform to multivariate images; we call it vectorial Dahu pseudo-distance. This new distance is easily and efficiently computed thanks to the multivariate tree of shapes (MToS). We propose an efficient way to compute this distance and its deduced saliency map in this thesis. We also investigate the properties of this distance in dealing with noise and blur in the image. This distance has been proved to be robust for pixel invariant. To validate this new distance, we provide benchmarks demonstrating how the vectorial Dahu pseudo-distance is more robust and competitive compared to other MB-based distances. This distance is promising for salient object detection, shortest path finding, and object segmentation. Moreover, we apply this distance to detect the document in videos. Our method is a region-based approach which relies on visual saliency deduced from the Dahu pseudo-distance. We show that the performance of our method is competitive with state-of-the-art methods on the ICDAR Smartdoc 2015 Competition dataset.

Continue reading

A two-stage temporal-like fully convolutional network framework for left ventricle segmentation and quantification on MR images

Abstract

Automatic segmentation of the left ventricle (LV) of a living human heart in a magnetic resonance (MR) image (2D+t) allows to measure some clinical significant indices like the regional wall thicknesses (RWT), cavity dimensions, cavity and myocardium areas, and cardiac phase. Here, we propose a novel framework made of a sequence of two fully convolutional networks (FCN). The first is a modified temporal-like VGG16 (the “localization network”) and is used to localize roughly the LV (filled-in) epicardium position in each MR volume. The second FCN is a modified temporal-like VGG16 too, but devoted to segment the LV myocardium and cavity (the “segmentation network”). We evaluate the proposed method with 5-fold-cross-validation on the MICCAI 2019 LV Full Quantification Challenge dataset. For the network used to localize the epicardium, we obtain an average dice index of 0.8953 on validation set. For the segmentation network, we obtain an average dice index of 0.8664 on validation set (there, data augmentation is used). The mean absolute error (MAE) of average cavity and myocardium areas, dimensions, RWT are 114.77 mm^2; 0.9220 mm; 0.9185 mm respectively. The computation time of the pipeline is less than 2 s for an entire 3D volume. The error rate of phase classification is 7.6364%, which indicates that the proposed approach has a promising performance to estimate all these parameters.

Continue reading

Learning endmember dynamics in multitemporal hyperspectral data using a state-space model formulation

Abstract

Hyperspectral image unmixing is an inverse problem aiming at recovering the spectral signatures of pure materials of interest (called endmembers) and estimating their proportions (called abundances) in every pixel of the image. However, in spite of a tremendous applicative potential and the avent of new satellite sensors with high temporal resolution, multitemporal hyperspectral unmixing is still a relatively underexplored research avenue in the community, compared to standard image unmixing. In this paper, we propose a new framework for multitemporal unmixing and endmember extraction based on a state-space model, and present a proof of concept on simulated data to show how this representation can be used to inform multitemporal unmixing with external prior knowledge, or on the contrary to learn the dynamics of the quantities involved from data using neural network architectures adapted to the identification of dynamical systems.

Continue reading