The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants & results
In Proceedings sixth workshop on synthesis
PaInleSS: A framework for parallel SAT solving
In Proceedings of the 20th international conference on theory and applications of satisfiability testing (SAT’17)
Abstract
Over the last decade, parallel SAT solving has been widely studied from both theoretical and practical aspects. There are now numerous solvers that dier by parallelization strategies, programming languages, concurrent programming, involved libraries, etc. Hence, comparing the eciency of the theoretical approaches is a challenging task. Moreover, the introduction of a new approach needs either a deep understanding of the existing solvers, or to start from scratch the implementation of a new tool. We present PaInleSS: a framework to build parallel SAT solvers for many-core environments. Thanks to its genericity and modularity, it provides the implementation of basics for parallel SAT solving like clause exchanges, Portfolio and Divide-and-Conquer strategies. It also enables users to easily create their own parallel solvers based on new strategies. Our experiments show that our framework compares well with some of the best state-of-the-art solvers.
Augmented songbook: An augmented reality educational application for raising music awareness
In Multimedia Tools and Applications
Abstract
This paper presents the development of an Augmented Reality mobile application which aims at sensibilizing young children to abstract concepts of music. Such concepts are, for instance, the musical notation or the concept of rythm. Recent studies in Augmented Reality for education suggest that such technologies have multiple benefits for students, including younger ones. As mobile document image acquisition and processing gains maturity on mobile platforms, we explore how it is possible to build a markerless and real-time application to augment the physical documents with didactical animations and interactive content. Given a standard image processing pipeline, we compare the performance of different local descriptors at two key stages of the process. Results suggest alternatives to the SIFT local descriptors, regarding result quality and computationnal efficiency, both for document model identification and pespective transform estimation. All experiments are performed on an original and public dataset we introduce here.
Caractérisation des zones de mouvement périodiques pour applications bio-médicales
In Actes du 26e colloque GRETSI
Abstract
De nombreuses applications biomedicales impliquent l’analyse de séquences pour la caractérisation du mouvement. Dans cet article, nous considerons des séquences 2D+t où un mouvement particulier (par exemple un flux sanguin) est associé à une zone spécifique de l’image 2D (par exemple une artère). Mais de nombreux mouvements peuvent co-exister dans les séquences (par exemple, il peut y avoir plusieurs vaisseaux sanguins presents, chacun avec leur flux spécifique). La caractérisation de ce type de mouvement implique d’abord de trouver les zones où le mouvement est présent, puis d’analyser ces mouvements : vitesse, régularité, fréquence, etc. Dans cet article, nous proposons une méthode appropriée pour détecter et caractériser simultanément les zones où le mouvement est présent dans une séquence. Nous pouvons ensuite classer ce mouvement en zones cohérentes en utilisant un apprentissage non supervisé et produire des métriques directement utilisables pour diverses applications. Nous illustrons et validons cette même méthode sur l’analyse du flux sanguin chez l’embryon de poisson.
Segmentation d’IRM de cerveaux de nouveau-nés en quelques secondes à l’aide d’un réseau de neurones convolutif <i>pseudo-3D</i> et de transfert d’apprentissage
In Actes du 26e colloque GRETSI
Abstract
L’imagerie par résonance magnétique (IRM) du cerveau est utilisée sur les nouveau-nés pour évaluer l’évolution du cerveau et diagnostiquer des maladies neurologiques. Ces examens nécessitent souvent une analyse quantitative des différents tissus du cerveau, de sorte qu’avoir une segmentation précise est essentiel. Dans cet article, nous proposons une méthode automatique rapide de segmentation en différents tissus des images IRM 3D de cerveaux de nouveau-nés ; elle utilise un réseau de neurones totalement convolutif (FCN) et du transfert d’apprentissage. Par rapport aux approches similaires qui reposent soit sur des patchs 2D ou 3D, soit sur des FCN totalement 3D, notre méthode est beaucoup plus rapide : elle ne prend que quelques secondes, et une seule modalité (T2) est nécessaire. Afin de prendre les informations 3D en compte, trois coupes 2D successives sont empilées pour former une image 2D en couleurs, dont l’ensemble sur tout le volume sert d’entrée à un FCN, pré-entraîné sur ImageNet pour la classification d’images naturelles. Nos expériences sur un ensemble de données de référence montrent que notre méthode obtient des résultats du niveau de ceux de l’état de l’art.
From neonatal to adult brain MR image segmentation in a few seconds using 3D-like fully convolutional network and transfer learning
In Proceedings of the 23rd IEEE international conference on image processing (ICIP)
Abstract
Brain magnetic resonance imaging (MRI) is widely used to assess brain developments in neonates and to diagnose a wide range of neurological diseases in adults. Such studies are usually based on quantitative analysis of different brain tissues, so it is essential to be able to classify them accurately. In this paper, we propose a fast automatic method that segments 3D brain MR images into different tissues using fully convolutional network (FCN) and transfer learning. As compared to existing deep learning-based approaches that rely either on 2D patches or on fully 3D FCN, our method is way much faster: it only takes a few seconds, and only a single modality (T1 or T2) is required. In order to take the 3D information into account, all 3 successive 2D slices are stacked to form a set of 2D color images, which serve as input for the FCN pre-trained on ImageNet for natural image classification. To the best of our knowledge, this is the first method that applies transfer learning to segment both neonatal and adult brain 3D MR images. Our experiments on two public datasets show that our method achieves state-of-the-art results.
Parallel learning portfolio-based solvers
In Proceedings of the international conference on computational science (ICCS)
Abstract
Exploiting multi-core architectures is a way to tackle the CPU time consumption when solving SAT- isfiability (SAT) problems. Portfolio is one of the main techniques that implements this principle. It consists in making several solvers competing, on the same problem, and the winner will be the first that answers. In this work, we improved this technique by using a learning schema, namely the Exploration- Exploitation using Exponential weight (EXP3), that allows smart resource allocations. Our contribution is adapted to situations where we have to solve a bench of SAT instances issued from one or several sequence of problems. Our experiments show that our approach achieves good results.
Well-composedness in Alexandrov spaces implies digital well-composedness in $Z^n$
In Discrete geometry for computer imagery – proceedings of the 20th IAPR international conference on discrete geometry for computer imagery (DGCI)
Abstract
In digital topology, it is well-known that, in 2D and in 3D, a digital set $X \subseteq Z^n$ is digitally well-composed (DWC), i.e., does not contain any critical configuration, if its immersion in the Khalimsky grids $H^n$ is well-composed in the sense of Alexandrov (AWC), i.e., its boundary is a disjoint union of discrete $(n-1)$-surfaces. We show that this is still true in $n$-D, $n \geq 2$, which is of prime importance since today 4D signals are more and more frequent.
Explicit state model checking with generalized büchi and rabin automata
In Proceedings of the 24th international SPIN symposium on model checking of software (SPIN’17)
Abstract
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 transition-based generalized Rabin automata (TGRAs), 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. We observed that our algorithm can be used to replace a TGBA checking algorithm without losing performance. In general, we found little to no improvement by checking TGRAs directly.
Object tracking by hierarchical decomposition of hyperspectral video sequences: Application to chemical gas plume tracking
In IEEE Transactions on Geoscience and Remote Sensing
Abstract
It is now possible to collect hyperspectral video sequences at a near real-time frame rate. The wealth of spectral, spatial and temporal information of those sequences is appealing for various applications, but classical video processing techniques must be adapted to handle the high dimensionality and huge size of the data to process. In this article, we introduce a novel method based on the hierarchical analysis of hyperspectral video sequences to perform object tracking. This latter operation is tackled as a sequential object detection process, conducted on the hierarchical representation of the hyperspectral video frames. We apply the proposed methodology to the chemical gas plume tracking scenario and compare its performances with state-of-the-art methods, for two real hyperspectral video sequences, and show that the proposed approach performs at least equally well.