Publications

Performance comparison of several folding strategies

Abstract

In this article we examine the computation order and consequent performance of three different conceptual implementations of the fold function. We explore a set of performance based experiments on different implementations of this function. In particular, we contrast the fold-left implementation with two other implements we refer to as pair-wise-fold and tree-like-fold. We explore two application areas: ratio arithmetic and Binary Decisions Diagram construction. We demonstrate several cases where the performance of certain algorithms is very different depending on the approach taken. In particular iterative computations where the object size accumulates are good candidates for the tree-like-fold.

Continue reading

Use of machine learning and infrared spectra for rheological characterization and application to the apricot

Abstract

Continue reading

Quickref: Common Lisp reference documentation as a stress test for Texinfo

Abstract

Quickref is a global documentation project for the Common Lisp ecosystem. It creates reference manuals automatically by introspecting libraries and generating corresponding documentation in Texinfo format. The Texinfo files may subsequently be converted into PDF or HTML. Quickref is non-intrusive: software developers do not have anything to do to get their libraries documented by the system.Quickref may be used to create a local website documenting your current, partial, working environment, but it is also able to document the whole Common Lisp ecosystem at once. The result is a website containing almost two thousand reference manuals. Quickref provides a Docker image for an easy recreation of this website, but a public version is also available and actively maintained.Quickref constitutes an enormous and successful stress test for Texinfo. In this paper, we give an overview of the design and architecture of the system, describe the challenges and difficulties in generating valid Texinfo code automatically, and put some emphasis on the currently remaining problems and deficiencies.

Continue reading

State-of-the-art speaker recognition for telephone and video speech: The JHU-MIT submission for NIST SRE18

Abstract

Continue reading

Non-linear dynamics analysis of protein sequences. Application to CYP450

Abstract

Continue reading

Connected filters on generalized shape-spaces

Abstract

Classical hierarchical image representations and connected filters work on sets of connected components (CC). These approaches can be defective to describe the relations between disjoint objects or partitions on images. In practice, objects can be made of several connected components in images (due to occlusions for example), therefore it can be interesting to be able to take into account the relationship between these components to be able to detect the whole object. In Mathematical Morphology, second-generation connectivity (SGC) and tree-based shape-space study this relation between the connected components of an image. However, they have limitations. For this reason, we propose in this paper an extension of the usual shape-space paradigm into what we call a Generalized Shape-Space (GSS). This new paradigm allows to analyze any graph of connected components hierarchically and to filter them thanks to connected operators.

Continue reading

Advanced ports toolkit: Near-perfect packing-list generation

Abstract

Continue reading

Combining parallel emptiness checks with partial order reductions

Abstract

In explicit state model checking ofconcurrent systems, multicore 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 prop- erties that relies on other multi-core emptiness checks. We observe that all presented algorithms maintain good reductions and scalability.

Continue reading

Generic emptiness check for fun and profit

Abstract

We present a new algorithm for checking the emptiness of $\omega$-automata with an Emerson-Lei acceptance condition (i.e., a positive Boolean formula over sets of states or transitions that must be visited infinitely or finitely often). The algorithm can also solve the model checking problem of probabilistic positiveness of MDP under a property given as a deterministic Emerson-Lei automaton. Although both these problems are known to be NP-complete and our algorithm is exponential in general, it runs in polynomial time for simpler acceptance conditions like generalized Rabin, Streett, or parity. In fact, the algorithm provides a unifying view on emptiness checks for these simpler automata classes. We have implemented the algorithm in Spot and PRISM and our experiments show improved performance over previous solutions.

Continue reading

Towards more efficient parallel SAT solving

Abstract

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.

Continue reading