In the context of software engineering for image processing (IP), we consider the notion of reusability of algorithms. In many software tools, an algorithm’s implementation often depends on the type of processed data. In a broad definition, discrete digital images may have various forms—classical 2D images, 3D volumes, non-regular graphs, cell complexes, and so on—thus leading to a combinatorial explosion of the theoretical number of implementations. Generic programming (GP) is a framework suited to the development of reusable software tools. We present a programming paradigm based on GP designed for the creation of scientific software such as IP tools. This approach combines the benefits of reusability, expressive power, extensibility, and efficiency. We then propose a software architecture for IP using this programming paradigm based on a generic IP library. The foundations of this framework define essential IP concepts, enabling the development of algorithms compatible with many image types. We finally present a strategy to build high-level tools on top of this library, such as bridges to dynamic languages or graphical user interfaces. This mechanism has been designed to preserve the genericity and efficiency of the underlying software tools, while making them simpler to use and more flexible.

We present the <i>Self-Loop Aggregation Product</i> (SLAP), a new hybrid technique that replaces the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed product is an explicit graph of aggregates (symbolic sets of states) that can be interpreted as a Büchi automata. The criterion used by SLAP to aggregate states from the Kripke structure is based on the analysis of self-loops that occur in the Büchi automaton expressing the property to verify. Our hybrid approach allows on the one hand to use classical emptiness-check algorithms and build the graph on-the-fly, and on the other hand, to have a compact encoding of the state space thanks to the symbolic representation of the aggregates. Our experiments show that this technique often outperforms other existing (hybrid or fully symbolic) approaches.

Spot is a library of model-checking algorithms. This paper focuses on the module translating LTL formulæ into automata. We discuss improvements that have been implemented in the last four years, we show how Spot’s translation competes on various benchmarks, and we give some insight into its implementation.

Electronic documents are being more and more usable thanks to better and more affordable network, storage and computational facilities. But in order to benefit from computer-aided document management, paper documents must be digitized and analyzed. This task may be challenging at several levels. Data may be of multiple types thus requiring different adapted processing chains. The tools to be developed should also take into account the needs and knowledge of users, ranging from a simple graphical application to a complete programming framework. Finally, the data sets to process may be large. In this paper, we expose a set of features that a Document Image Analysis framework should provide to handle the previous issues. In particular, a good strategy to address both flexibility and efficiency issues is the Generic Programming (GP) paradigm. These ideas are implemented as an open source module, SCRIBO, built on top of Olena, a generic and efficient image processing platform. Our solution features services such as preprocessing filters, text detection, page segmentation and document reconstruction (as XML, PDF or HTML documents). This framework, composed of reusable software components, can be used to create full-fledged graphical applications, small utilities, or processing chains to be integrated into third-party projects.

De plus en plus d’outils logiciels modernes pour le traitement d’images sont conçus en prenant en compte le problème de la généricité du code, c’est-à-dire la possibilité d’écrire des algorithmes réutilisables, compatibles avec de nombreux types d’entrées. Cependant, ce choix de conception se fait souvent au détriment des performances du code exécuté. Du fait de la grande variété des types d’images existants et de la nécessité d’avoir des implémentations rapides, généricité et performance apparaissent comme des qualités essentielles du logiciel en traitement d’images. Cet article présente une approche préservant les performances dans un framework logiciel générique tirant parti des caractéristiques des types de données utilisés. Grâce à celles-ci, il est possible d’écrire des variantes d’algorithmes génériques offrant un compromis entre généricité et performance. Ces alternatives sont capables de préserver une partie des aspects génériques d’origine tout en apportant des gains substantiels à l’exécution. D’après nos essais, ces optimisations génériques fournissent des performances supportant la comparaison avec du code dédié, allant parfois même jusqu’à surpasser des routines optimisées manuellement.

Geldenhuys and Hansen have shown that a kind of $\omega$-automaton known as <i>testing automata</i> can outperform the Buchi automata traditionally used in the automata-theoretic approach to model checking (<b>geldenhuys.06.spin?</b>). This work completes their experiments by including a comparison with generalized Buchi automata; by using larger state spaces derived from Petri nets; and by distinguishing violated formulæ (for which testing automata fare better) from verified formulæ (where testing automata are hindered by their two-pass emptiness check).

We present two new hybrid techniques that replace the synchronized product used in the automata-theoretic approach for LTL model checking. The proposed products are explicit graphs of aggregates (symbolic sets of states) that can be interpreted as Büchi automata. These hybrid approaches allow on the one hand to use classical emptiness-check algorithms and build the graph on-the-fly, and on the other hand, to have a compact encoding of the state space thanks to the symbolic representation of the aggregates. The <i>Symbolic Observation Product</i> assumes a globally stuttering property (e.g., LTL-X) to aggregate states. The <i>Self-Loop Aggregation Product</i> does not require the property to be globally stuttering (i.e., it can tackle full LTL), but dynamically detects and exploits a form of stuttering where possible. Our experiments show that these two variants, while incomparable with each other, can outperform other existing approaches.