Détail d'une fiche   Version PDF

OLAS (SR0949SR)

Fondements opérationnels, logiques et algébriques des systèmes logiciels

FOCUS (SR0400XR) →  OLAS


Statut: Décision signée

Responsable : Davide Sangiorgi

Mots-clés de "A - Thèmes de recherche en Sciences du numérique - 2024" : A1.3. Systèmes distribués , A1.4. Systèmes ubiquitaires , A2. Logiciel , A2.1. Langages de programmation , A2.1.1. Sémantique des langages de programmation , A2.1.4. Programmation fonctionnelle , A2.1.6. Programmation concurrente , A2.1.7. Programmation distribuée , A2.4. Méthodes formelles pour vérification, sureté, certification , A2.4.1. Analyse , A2.4.3. Preuves , A7. Informatique théorique , A7.2. Logique

Mots-clés de "B - Autres sciences et domaines d'application - 2024" : B6.1. Industrie du logiciel , B6.3. Fonctions réseaux , B6.4. Internet des objets , B9.5.1. Informatique

Domaine : Algorithmique, programmation, logiciels et architectures
Thème : Preuves et vérification

Période : 01/10/2023 -> 30/09/2027
Dates d'évaluation :

Etablissement(s) de rattachement : U. DE BOLOGNE - UNIBO (ITALIE)
Laboratoire(s) partenaire(s) : <sans UMR>

CRI : Centre Inria d'Université Côte d'Azur
Localisation : Centre Inria d'Université Côte d'Azur
Code structure Inria : 041174-0

Numéro RNSR : 202324453J
N° de structure Inria: SR0949SR

Présentation

Le logiciel transforme de plus en plus notre vie quotidienne. Mais les applications deviennent aussi de plus en plus complexes. Cela pose d'énormes défis lorsqu'il s'agit de garantir que les logiciels fonctionnent correctement et efficacement. La correction consiste en garantir qu'un programme répond aux exigences attendues. L'efficacité consiste en mieux contrôler l'utilisation des ressources lors de l'exécution d'un programme, et ce sans affecter le comportement global.

Au sein d'Olas, nous étudions des modèles et des techniques permettant de raisonner sur la correction et sur l'efficacité des systèmes logiciels modernes. Nous nous concentrons sur les langages et les formalismes d'ordre supérieur, au sens où ceux-ci permettent, syntaxiquement ou sémantiquement, la représentation de fonctions générales, y compris des fonctions qui prennent d'autres fonctions comme arguments. Une spécificité des langages d'ordre supérieur est qu'ils sont ouverts : la visibilité qu'un terme a de son environnement peut changer au fil du temps, car l'interaction du terme avec son environnement affectera les capacités futures en termes d'interactions. Une autre caractéristique est la possibilité d'abstraire, à la fois vis-à-vis des données et vis-à-vis du comportement. Les constructions d'ordre supérieur sont importantes dans les langages de programmation de haut niveau modernes. Par exemple, les logiciels sont généralement ouverts car ils s'exécutent en réseau ; et l'abstraction est importante pour écrire du code concis et pour améliorer la modularité. En effet, les langages de programmation modernes incluent normalement des constructions d'ordre supérieur.


Axes de recherche

Ll'objectif d'Olas est le développement de la sémantique, de concepts, de techniques et, le cas échant, de constructions et de langages de programmation, pour spécifier et raisonner sur des systèmes logiciels d'ordre supérieur. La modélisation est fondamentale pour ces activités. Les modèles que nous étudions s'inscrivent dans la tradition du lambda-calcul et des calculs de processus. Ces modèles, qui mettent l'accent sur l'algèbre, se prêtent bien à des traitements compositionnels, une propriété centrale dans notre approche des problèmes. En conséquence, les techniques que nous utilisons sont principalement des techniques opérationnelles, fondées sur des notions d'équivalence et d'approximation comportementales, ainsi que des techniques fondées sur l'algèbre, la logique mathématique et la théorie des types.


Relations industrielles et internationales

Nous coopérons avec diverses équipes Inria, dont Splits, Spades, Spirals, avec les universités ENS Lyon, Paris VII, Cambridge, Copenhague, Munich, Lisbonne, Tokyo, et d'autres. Nous participons à quelques initiatives et projets européens et nationaux, impliquant également certaines industries.