Publications

Go2Pins: A framework for the LTL verification of Go programs

By Alexandre Kirszenberg, Antoine Martin, Hugo Moreau, Étienne Renault

2021-06-08

In Proceedings of the 27th international SPIN symposium on model checking of software (SPIN’21)

Abstract

We introduce Go2Pins, a tool that takes a program written in Go and links it with two model-checkers: LTSMin [19] and Spot [7]. Go2Pins is an effort to promote the integration of both formal verifica- tion and testing inside industrial-size projects. With this goal in mind, we introduce black-box transitions, an efficient and scalable technique for handling the Go runtime. This approach, inspired by hardware ver- ification techniques, allows easy, automatic and efficient abstractions. Go2Pins also handles basic concurrent programs through the use of a dedicated scheduler. In this paper we demonstrate the usage of Go2Pins over benchmarks inspired by industrial problems and a set of LTL formulae. Even if Go2Pins is still at the early stages of development, our results are promising and show the the benefits of using black-box transitions.

Continue reading

ICDAR 2021 competition on historical map segmentation

By Joseph Chazalon, Edwin Carlinet, Yizi Chen, Julien Perret, Bertrand Duménieu, Clément Mallet, Thierry Géraud, Vincent Nguyen, Nam Nguyen, Josef Baloun, Ladislav Lenc, Pavel Král

2021-05-17

In Proceedings of the 16th international conference on document analysis and recognition (ICDAR’21)

Abstract

This paper presents the final results of the ICDAR 2021 Competition on Historical Map Segmentation (MapSeg), encouraging research on a series of historical atlases of Paris, France, drawn at 1/5000 scale between 1894 and 1937. The competition featured three tasks, awarded separately. Task 1 consists in detecting building blocks and was won by the L3IRIS team using a DenseNet-121 network trained in a weakly supervised fashion. This task is evaluated on 3 large images containing hundreds of shapes to detect. Task 2 consists in segmenting map content from the larger map sheet, and was won by the UWB team using a U-Net-like FCN combined with a binarization method to increase detection edge accuracy. Task 3 consists in locating intersection points of geo-referencing lines, and was also won by the UWB team who used a dedicated pipeline combining binarization, line detection with Hough transform, candidate filtering, and template matching for intersection refinement. Tasks 2 and 3 are evaluated on 95 map sheets with complex content. Dataset, evaluation tools and results are available under permissive licensing at https://icdar21-mapseg.github.io/.

Continue reading

Revisiting the Coco panoptic metric to enable visual and qualitative analysis of historical map instance segmentation

By Joseph Chazalon, Edwin Carlinet

2021-05-17

In Proceedings of the 16th international conference on document analysis and recognition (ICDAR’21)

Abstract

Segmentation is an important task. It is so important that there exist tens of metrics trying to score and rank segmentation systems. It is so important that each topic has its own metric because their problem is too specific. Does it? What are the fundamental differences with the ZoneMap metric used for page segmentation, the COCO Panoptic metric used in computer vision and metrics used to rank hierarchical segmentations? In this paper, while assessing segmentation accuracy for historical maps, we explain, compare and demystify some the most used segmentation evaluation protocols. In particular, we focus on an alternative view of the COCO Panoptic metric as a classification evaluation; we show its soundness and propose extensions with more “shape-oriented” metrics. Beyond a quantitative metric, this paper aims also at providing qualitative measures through precision-recall maps that enable visualizing the success and the failures of a segmentation method.

Continue reading

Vectorization of historical maps using deep edge filtering and closed shape extraction

By Yizi Chen, Edwin Carlinet, Joseph Chazalon, Clément Mallet, Bertrand Duménieu, Julien Perret

2021-05-17

In Proceedings of the 16th international conference on document analysis and recognition (ICDAR’21)

Abstract

Maps have been a unique source of knowledge for centuries. Such historical documents provide invaluable information for analyzing the complex spatial transformation of landscapes over important time frames. This is particularly true for urban areas that encompass multiple interleaved research domains (social sciences, economy, etc.). The large amount and significant diversity of map sources call for automatic image processing techniques in order to extract the relevant objects under a vectorial shape. The complexity of maps (text, noise, digitization artifacts, etc.) has hindered the capacity of proposing a versatile and efficient raster-to-vector approaches for decades. We propose a learnable, reproducible, and reusable solution for the automatic transformation of raster maps into vector objects (building blocks, streets, rivers). It is built upon the complementary strength of mathematical morphology and convolutional neural networks through efficient edge filtering. Evenmore, we modify ConnNet and combine with deep edge filtering architecture to make use of pixel connectivity information and built an end-to-end system without requiring any post-processing techniques. In this paper, we focus on the comprehensive benchmark on various architectures on multiple datasets coupled with a novel vectorization step. Our experimental results on a new public dataset using COCO Panoptic metric exhibit very encouraging results confirmed by a qualitative analysis of the success and failure cases of our approach. Code, dataset, results and extra illustrations are freely available at https://github.com/soduco/ICDAR-2021-Vectorization.

Continue reading

Learning Sentinel-2 spectral dynamics for long-run predictions using residual neural networks

By Joaquim Estopinan, Guillaume Tochon, Lucas Drumetz

2021-05-04

In Proceedings of the 29th european signal processing conference (EUSIPCO)

Abstract

Making the most of multispectral image time-series is a promising but still relatively under-explored research direction because of the complexity of jointly analyzing spatial, spectral and temporal information. Capturing and characterizing temporal dynamics is one of the important and challenging issues. Our new method paves the way to capture real data dynamics and should eventually benefit applications like unmixing or classification. Dealing with time-series dynamics classically requires the knowledge of a dynamical model and an observation model. The former may be incorrect or computationally hard to handle, thus motivating data-driven strategies aiming at learning dynamics directly from data. In this paper, we adapt neural network architectures to learn periodic dynamics of both simulated and real multispectral time-series. We emphasize the necessity of choosing the right state variable to capture periodic dynamics and show that our models can reproduce the average seasonal dynamics of vegetation using only one year of training data.

Continue reading

A blockchain-based certificate revocation management and status verification system

By Elloh Adja, Badis Hammi, Ahmed Serhrouchni, Sherali Zeadally

2021-05-01

In Computers & Security

Abstract

Revocation management is one of the main tasks of the Public Key Infrastructure (PKI). It is also critical to the security of any PKI. As a result of the increase in the number and sizes of networks as well as the adoption of novel paradigms such as the Internet of Things and their usage of the web, current revocation mechanisms are vulnerable to single point of failures as the network loads increase. To address this challenge, we take advantage of blockchains power and resiliency in order to propose an efficient decentralized certificates revocation management and status verification system. We use the extension field of the X509 certificate’s structure to introduce a field that describes to which distribution point the certificate will belong to if revoked. Each distribution point is represented by a Bloom filter filled with revoked certificates. Bloom filters and revocation information are stored in a public blockchain. We developed a real implementation of our proposed mechanism in Python and the Namecoin blockchain. Then, we conducted an extensive evaluation of our scheme using performance metrics such as execution time and data consumption to demonstrate that it can meet the needed requirements with high efficiency and low cost. Moreover, we compare the performance of our approach with two of the most well-known/used revocation techniques which are Online Certificate Status Protocol (OCSP) and Certificate Revocation List (CRL). The results obtained show that our proposed approach outperforms these current schemes.

Continue reading

A corpus processing and analysis pipeline for Quickref

By Antoine Hacquard, Didier Verna

2021-05-01

In ELS 2021, the 14th european lisp symposium

Abstract

Quicklisp is a library manager working with your existing Common Lisp implementation to download and install around 2000 libraries, from a central archive. Quickref, an application itself written in Common Lisp, generates, automatically and by introspection, a technical documentation for every library in Quicklisp, and produces a website for this documentation. In this paper, we present a corpus processing and analysis pipeline for Quickref. This pipeline consists of a set of natural language processing blocks allowing us to analyze Quicklisp libraries, based on natural language contents sources such as README files, docstrings, or symbol names. The ultimate purpose of this pipeline is the generation of a keyword index for Quickref, although other applications such as word clouds or topic analysis are also envisioned.

Continue reading

A portable, simple, embeddable type system

By Jim Newton, Adrien Pommellet

2021-04-26

In ELS 2021, the 14th european lisp symposium

Abstract

We present a simple type system inspired by that of Common Lisp. The type system is intended to be embedded into a host language and accepts certain fundamental types from that language as axiomatically given. The type calculus provided in the type system is capable of expressing union, intersection, and complement types, as well as membership, subtype, disjoint, and habitation (non-emptiness) checks. We present a theoretical foundation and two sample implementations, one in Clojure and one in Scala.

Continue reading

An innovative and decentralized identity framework based on blockchain technology

By Daniel Maldonado-Ruiz, Jenny Torres, Nour El Madhoun, Mohamad Badra

2021-04-01

In 11th IFIP international conference on new technologies, mobility and security (NTMS)

Abstract

Network users usually need a third party validation to prove that they are who they claim to be. Authentication systems mostly assume the existence of a Trusted Third Party (TTP) in the form of a Certificate Authority (CA) or as an authentication server. However, relying on a TTP implies that users do not directly manage their identities, but delegate this role to a third party. This intrinsic issue can generate trust concerns (e.g., identity theft), as well as privacy concerns towards the third party. The main objective of this research is to present an autonomous and independent solution where users can store their self created credentials without depending on TTPs. To this aim, the use of an TTP autonomous and independent network is needed, where users can manage and assess their identities themselves. In this paper, we propose the framework called Three Blockchains Identity Management with Elliptic Curve Cryptography (3BI-ECC). With our proposed framework, the users’ identities are self-generated and validated by their owners. Moreover, it allows the users to customize the information they want to share with third parties.

Continue reading

A new matching algorithm between trees of shapes and its application to brain tumor segmentation

By Nicolas Boutry, Thierry Géraud

2021-03-02

In Proceedings of the IAPR international conference on discrete geometry and mathematical morphology (DGMM)

Abstract

Many approaches exist to compute the distance between two trees in pattern recognition. These trees can be structures with or without values on their nodes or edges. However, none of these distances take into account the shapes possibly associated to the nodes of the tree. For this reason, we propose in this paper a new distance between two trees of shapes based on the Hausdorff distance. This distance allows us to make inexact tree matching and to compute what we call residual trees, representing where two trees differ. We will also see that thanks to these residual trees, we can obtain good results in matter of brain tumor segmentation. This segmentation does not provide only a segmentation but also the tree of shapes corresponding to the segmentation and its depth map.

Continue reading

Search

Tags