Publications

Comparing use-cases of tree-fold vs fold-left, how to fold and color a map

Jim Newton

In this article we examine some consequences of computation order of two different conceptual implementations of the fold function. We explore a set of performance- and accuracy-based experiments on two implementations of this function. In particular, we contrast the traditional fold-left implementation with another approach we refer to as tree-fold. It is often implicitly supposed that the binary operation in question has constant complexity. We explore several application areas which diverge from that assumption: rational arithmetic, floating-point arithmetic, and Binary Decisions Diagram construction. These are binary operations which degrade in performance as the fold iteration progresses. We show that these types of binary operations are good candidates for tree-fold.

PhishGNN: A phishing website detection framework using graph neural networks

Tristan Bilot · Grégoire Geis · Badis Hammi

Because of the importance of the web in our daily lives, phishing attacks have been causing a significant damage to both individuals and organizations. Indeed, phishing attacks are today among the most widespread and serious threats to the web and its users. The main approaches deployed against such attacks are blacklists. However, the latter represents numerous drawbacks. In this paper, we introduce PhishGNN, a Deep Learning framework based on Graph Neural Networks, which leverages and uses the hyperlink graph structure of web- sites along with different other hand-designed features. The performance results obtained, demonstrate that PhishGNN outperforms state of the art results with a 99.7% prediction accuracy.

A hybrid optimization tool for active magnetic regenerator

Anna Ouskova Leonteva · Michel Risser · Radia Hamane · Anne Jeannin-Girardon · Pierre Parrend · Pierre Collet

real-world application
hybridization
unified optimization

Active Magnetic Regenerator (AMR) refrigeration is an innovate technology, which can reduce energy consumption and the depletion of the ozone layer. However, to develop a commercially applicable design of the AMR model is still an issue, because of the difficulty to find a configuration of the AMR parameters, which are suitable for various applications needs. In this work, we focus on the optimization method for finding a common parameters of the AMR model in two application modes: a magnetic refrigeration system and a thermo-magnetic generator. This paper proposes a robust optimisation tool, which ensures the scalability with respect to the number of objectives and allows to easily set up different optimisation experiments. A tool validation is presented. It is expected that this tool can help to make a qualitative jump in the development of AMR refrigeration.

What does my GNN really capture? On exploring internal GNN representations

Luca Veyrin-Forrer · Ataollah Kamal · Stefan Duffner · Marc Plantevit · Céline Robardet

GNNs are efficient for classifying graphs but their internal workings is opaque which limits their field of application. Existing methods for explaining GNN focus on disclosing the relationships between input graphs and the model’s decision. In contrary, the method we propose isolates internal features, hidden in the network layers, which are automatically identified by the GNN to classify graphs. We show that this method makes it possible to know the parts of the input graphs used by GNN with much less bias than the SOTA methods and therefore to provide confidence in the decision process.

Survey on smart homes: Vulnerabilities, risks, and countermeasures

Badis Hammi · Sherali Zeadally · Rida Khatoun · Jamel Nebhen

Over the last few years, the explosive growth of Internet of Things (IoT) has revolutionized the way we live and interact with each other as well as with various types of systems and devices which form part of the Information Communication Technology (ICT) infrastructure. IoT is having a significant impact on various application domains including healthcare, smart home, transportation, energy, agriculture, manufacturing, and many others. We focus on the smart home environment which has attracted a lot of attention from both academia and industry recently. The smart home provides a lot of convenience to home users but it also opens up various risks that threaten both the security and privacy of the users. In contrast to previous works on smart home security and privacy, we present an overview of smart homes from both academic and industry perspectives. Next we discuss the security requirements, challenges and threats associated with smart homes. Finally, we discuss countermeasures that can be deployed to mitigate the identified threats.

The reactive synthesis competition (SYNTCOMP): 2018-2021

Swen Jacobs · Guillermo Alberto Perez · Remco Abraham · Véronique Bruyère · Michaël Cadilhac · Maximilien Colange · Charly Delfosse · Tom Dijk · Alexandre Duret-Lutz · Peter Faymonville · Bernd Finkbeiner · Ayrat Khalimov · Felix Klein · Michael Luttenberger · Klara J. Meyer · Thibaud Michaud · Adrien Pommellet · Florian Renkin · Philipp Schlehuber-Caissier · Mouhammad Sakr · Salomon Sickert · Gaëtan Staquet · Clément Tamines · Leander Tentrup · Adam Walker

Reactive synthesis
algorithmic verification
zero-sum games

LTL under reductions with weaker conditions than stutter invariance

Emmanuel Paviot-Adet · Denis Poitrenaud · Étienne Renault · Yann Thierry-Mieg

Verification of properties expressed as omega-regular languages such as LTL can benefit hugely from stutter insensitivity, using a diverse set of reduction strategies. However properties that are not stutter invariant, for instance due to the use of the neXt operator of LTL or to some form of counting in the logic, are not covered by these techniques in general. We propose in this paper to study a weaker property than stutter insensitivity. In a stutter insensitive language both adding and removing stutter to a word does not change its acceptance, any stuttering can be abstracted away; by decomposing this equivalence relation into two implications we obtain weaker conditions. We define a shortening insensitive language where any word that stutters less than a word in the language must also belong to the language. A lengthening insensitive language has the dual property. A semi-decision procedure is then introduced to reliably prove shortening insensitive properties or deny lengthening insensitive properties while working with a reduction of a system. A reduction has the property that it can only shorten runs. Lipton’s transaction reductions or Petri net agglomerations are examples of eligible structural reduction strategies. An implementation and experimental evidence is provided showing most non- random properties sensitive to stutter are actually shortening or lengthening in- sensitive. Performance of experiments on a large (random) benchmark from the model-checking competition indicate that despite being a semi-decision proce- dure, the approach can still improve state of the art verification tools. 1 Introduction Model checking is an automatic verification technique for proving the correctness of systems that have finite state abstractions. Properties can be expressed using the popular Linear-time Temporal Logic (LTL). To verify LTL properties, the automata-theoretic approach [25] builds a product between a Buchi automaton representing the negation of the LTL formula and the reachable state graph of the system (seen as a set of infinite runs). This approach has been used successfully to verify both hardware and software components, but it suffers from the so called "state explosion problem": as the number of state variables in the system increases, the size of the system state space grows exponentially.

Effective reductions of Mealy machines

Florian Renkin · Philipp Schlehuber-Caissier · Alexandre Duret-Lutz · Adrien Pommellet

We revisit the problem of reducing incompletely specified Mealy machines with reactive synthesis in mind. We propose two techniques: the former is inspired by the tool MeMin and solves the minimization problem, the latter is a novel approach derived from simulation-based reductions but may not guarantee a minimized machine. However, we argue that it offers a good enough compromise between the size of the resulting Mealy machine and performance. The proposed methods are benchmarked against <span style="font-variant:small-caps;">MeMin</span> on a large collection of test cases made of well-known instances as well as new ones.

A benchmark of named entity recognition approaches in historical documents

Nathalie Abadie · Edwin Carlinet · Joseph Chazalon · Bertrand Duménieu

Named entity recognition (NER) is a necessary step in many pipelines targeting historical documents. Indeed, such natural language processing techniques identify which class each text token belongs to, e.g. “person name”, “location”, “number”. Introducing a new public dataset built from 19th century French directories, we first assess how noisy modern, off-the-shelf OCR are. Then, we compare modern CNN- and Transformer-based NER techniques which can be reasonably used in the context of historical document analysis. We measure their requirements in terms of training data, the effects of OCR noise on their performance, and show how Transformer-based NER can benefit from unsupervised pre-training and supervised fine-tuning on noisy data. Results can be reproduced using resources available at https://github.com/soduco/paper-ner-bench-das22 and https://zenodo.org/record/6394464