Ongoing Projects

AcceptAlgo (2024-2025)

PI: Béatrice Boulu-Reshef (LEO, Laboratoire d’Economie d’Orléans)
co-PI: Frédéric Loulergue

AcceptAlgo is a two-year project funded by Région Centre Val de Loire.

Individuals have seen their exposure to algorithms increase considerably over the past decade. This exposure is exercised mainly in direct interaction with computers, telephones or other connected objects, during many moments of the social and economic life of individuals, but also in administrative or technical procedures of professionals. Individuals interact with algorithms when searching for information on the internet, when using connected medical devices, when delegating the management of their savings and retirement or when making online purchases. This research project aims to study how individuals evaluate and accept algorithms presented in mathematical form and in simple language form i.e. with words intelligible by individuals. It consists in measuring the acceptability for individuals of the algorithms presented through these simplified explanations.

SeSTeRce (2023-2024) 

PI: Jules Chouquet

SeSTeRce means “Sémantique des Systèmes Temporels et Réactifs” (Semantics of Timed and Reactive Systems). It is funded by Université d’Orléans in its BQR program.

The Internet of Things comes in the form of devices, most often connected to a multitude of other devices; these connections consist of a permanent and uninterrupted exchange of data. Some applications, in the medical field for example, require a very high degree of trust and security in the implemented software. The analysis and verification of these programs (known as reactive) is therefore a crucial issue, both scientific and social, at the heart of the themes of the PI. The project takes a fundamental and exploratory approach to these questions, from the point of view of theoretical and mathematical analyses. 

CoMeMoV (2023-2025) 

PI: Frédéric Loulergue

CoMeMoV is funded by ANR (ANR-22-CE25-0018) and is a joint project with CEA List and Thales Research & Technology.

While Frama-C was successfully used for deductive verification in various case studies, recent industrial applications conducted at Thales Research and Technology demonstrated the need for significant enhancements of the tool to make it possible to efficiently and soundly realise deductive verification of real-life industrial software products with >10k lines of code mixing complex data-structures, dynamic memory allocation and low-level constructs such as bitfields, unions and memory casts. The Frama-C/WP plugin provides a combination of different memory models that collaborate together thanks to a smart but simple partitioning of the memory. On moderately complex, industrial strength programs, this combination already makes WP mature enough to be deployed for proving industrial critical embedded software. However, several theoretical and practical issues still persist. The goal of CoMeMoV (Collaborative Memory Models for formal Verification) is to tackle these issues to scale on deductive verification of complex programs.

SIOMediC (2023-2024)

PI: Patrice Clemente (SDS team)
coPI: Frédéric Loulergue

SIOMediC is a project of INSA Centre Val de Loire and Université d’Orléans, funded by Région Centre Val de Loire.

Digital health and in particular Connected Medical Devices (CMD) are experiencing rapid growth. Unfortunately, the numerous and recurring vulnerabilities of these devices present major confidentiality problems for medical data and significant dangers for the physical integrity of individuals. Our work aims to make DMCs safer (free from software bugs) and more secure (resistant to external attacks). We want to propose new protocols for interconnecting DMCs in their environment (hospital or domestic) and access control models, adapted to these different uses (often wireless). The goal is then to protect the DMCs from external attacks. We also want to be able to provide guarantees that neither the codes (programs) embedded on the DMCs, nor the protocols and protection mechanisms that we add to them, present any vulnerabilities. The main deliverables will be reusable software components.

Past projects

DeSSUF (2022-2023)

PI: Frédéric Loulergue

DeSSUF means “A Methodology for the Design of a Safe, Secure and User-Friendly Reactive Programming Language for the Internet of Things”. DeSSUF is funded by ANR via the PIA3 project Athena European University. 

In the Internet of Things (IoT), billions of devices are connected. Very often, these devices are programmed with the C programming language, mostly because of the limited hardware resources of such objects. However, C is error-prone, and software bugs make devices both unreliable and vulnerable to cyber-attacks. Several cases of massive cyber-attacks using IoT devices are documented. Moreover, the IoT is more and more deployed in areas such as energy, transportation and health: it is of paramount importance such systems are reliable, safe and secure. The goal of the DeSSUF project is the design, implementation, and the evaluation of the safety, security and ease-of-use of a new programming language for the IoT.

This is a joint project between the University of Orleans, LIFO, France and the University of Maribor, LPM, Slovenia both members of the Athena European University.

Static Analysis of BSP Programs (2016-2019)

PI: Frédéric Loulergue
coPI: Frédéric Dabrowski and Wadoud Bousdira

In cooperation with Huawei we have conducted research on the static analysis and generation of imperative BSP (Bulk Synchronous Paradigm) programs.  The result of this parternship can be found in Arvid Jakobsson’s PhD thesis and in Thibaut Tachon’s PhD thesis.

Girafon (2015-2017)

PI: Frédéric Loulergue

The GIRAFON project was funded by the Centre Val de Loire Region (APR-IA GIRAFON) and was a joint project with the CA, PAMDA, SDS Teams of LIFO, and LIFAT, Université de Tours.

The objective of the GIRAFON project was to design generic algorithms for mining large graphs based on a rich query language and distributed execution environments accompanied by dedicated programming libraries, while taking into account the protection of the privacy of individuals.

This objective was divided into four tasks which led to the development of software prototypes serving as proof of concept of the relevance of the proposed approaches, and which were evaluated in distributed computing environments: